(set-logic QF_NRA)
(declare-const v0 Bool)
(declare-const v1 Bool)
(declare-const v2 Bool)
(declare-const v3 Bool)
(declare-const v4 Bool)
(declare-const v5 Bool)
(declare-const v6 Bool)
(declare-const v7 Bool)
(declare-const v8 Bool)
(declare-const v9 Bool)
(declare-const v10 Bool)
(declare-const v11 Bool)
(declare-const v12 Bool)
(declare-const v13 Bool)
(declare-const v14 Bool)
(declare-const v15 Bool)
(declare-const v16 Bool)
(declare-const r0 Real)
(declare-const r1 Real)
(declare-const v17 Bool)
(declare-const v18 Bool)
(declare-const r2 Real)
(declare-const r3 Real)
(declare-const v19 Bool)
(declare-const r4 Real)
(declare-const v20 Bool)
(declare-const v21 Bool)
(declare-const v22 Bool)
(declare-const r5 Real)
(declare-const v23 Bool)
(declare-const r6 Real)
(declare-const v24 Bool)
(declare-const v25 Bool)
(declare-const v26 Bool)
(declare-const v27 Bool)
(declare-const v28 Bool)
(declare-const v29 Bool)
(declare-const v30 Bool)
(declare-const v31 Bool)
(declare-const v32 Bool)
(declare-const v33 Bool)
(declare-const v34 Bool)
(declare-const r7 Real)
(declare-const v35 Bool)
(declare-const v36 Bool)
(declare-const v37 Bool)
(declare-const v38 Bool)
(declare-const v39 Bool)
(declare-const v40 Bool)
(declare-const v41 Bool)
(declare-const v42 Bool)
(declare-const v43 Bool)
(declare-const r8 Real)
(declare-const v44 Bool)
(declare-const v45 Bool)
(declare-const r9 Real)
(declare-const v46 Bool)
(declare-const v47 Bool)
(declare-const v48 Bool)
(declare-const v49 Bool)
(declare-const r10 Real)
(declare-const v50 Bool)
(declare-const v51 Bool)
(declare-const r11 Real)
(declare-const v52 Bool)
(declare-const r12 Real)
(declare-const v53 Bool)
(declare-const v54 Bool)
(declare-const v55 Bool)
(declare-const r13 Real)
(declare-const v56 Bool)
(declare-const r14 Real)
(declare-const v57 Bool)
(declare-const v58 Bool)
(declare-const r15 Real)
(declare-const v59 Bool)
(declare-const v60 Bool)
(declare-const r16 Real)
(declare-const v61 Bool)
(declare-const v62 Bool)
(declare-const v63 Bool)
(declare-const r17 Real)
(declare-const v64 Bool)
(declare-const v65 Bool)
(declare-const v66 Bool)
(declare-const v67 Bool)
(declare-const r18 Real)
(assert (or v44 v30 v30))
(assert (or v39 (<= (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (+ (- (* 26664.0 (* r1 r0 83.0 83.0) (/ r0 (/ 83.0 r2)) r1 (* r1 (* r1 r0 83.0 83.0) r1 r1)) 26664.0 83.0) (/ r8 6618424257.0) r2 26664.0) (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (/ r5 (/ (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (* 26664.0 (* r1 r0 83.0 83.0) (/ r0 (/ 83.0 r2)) r1 (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (* (- r2) (* r1 r0 83.0 83.0) r2 (/ 83.0 r2))) v5))
(assert (or v60 (distinct (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1))))) (<= 26664.0 (- r1))))
(assert (or v26 v30 v5))
(assert (or (<= 26664.0 (- r1)) (<= (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (+ (- (* 26664.0 (* r1 r0 83.0 83.0) (/ r0 (/ 83.0 r2)) r1 (* r1 (* r1 r0 83.0 83.0) r1 r1)) 26664.0 83.0) (/ r8 6618424257.0) r2 26664.0) (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (/ r5 (/ (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (* 26664.0 (* r1 r0 83.0 83.0) (/ r0 (/ 83.0 r2)) r1 (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (* (- r2) (* r1 r0 83.0 83.0) r2 (/ 83.0 r2))) v39))
(assert (or v5 v38 (<= (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (+ (- (* 26664.0 (* r1 r0 83.0 83.0) (/ r0 (/ 83.0 r2)) r1 (* r1 (* r1 r0 83.0 83.0) r1 r1)) 26664.0 83.0) (/ r8 6618424257.0) r2 26664.0) (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (/ r5 (/ (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (* 26664.0 (* r1 r0 83.0 83.0) (/ r0 (/ 83.0 r2)) r1 (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (* (- r2) (* r1 r0 83.0 83.0) r2 (/ 83.0 r2)))))
(assert (or v38 (xor (>= (* r1 (* r1 r0 83.0 83.0) r1 r1) 2426.0 2426.0 6618424257.0) v59 v7) (and (and v12 v11 (>= 307769.0 r5) v40 (>= r6 (/ r0 (/ 83.0 r2)) (+ r1 r3 (* r1 r0 83.0 83.0) r2 r0) (* (- (* 26664.0 (* r1 r0 83.0 83.0) (/ r0 (/ 83.0 r2)) r1 (* r1 (* r1 r0 83.0 83.0) r1 r1)) 26664.0 83.0) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (<= (* (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)) r2 (* r1 (* r1 r0 83.0 83.0) r1 r1) (* r1 (* r1 r0 83.0 83.0) r1 r1) 6618424257.0) 2.0 (* (/ r0 (/ 83.0 r2)) 2.0 r6 (* r1 r0 83.0 83.0))) (<= (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1))) (/ r8 6618424257.0)) v30) (and (= (* r1 r0 83.0 83.0) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)) r1) (>= 83.0 r2 (* r1 (* r1 r0 83.0 83.0) r1 r1) r1 83.0) v1 v10 v18 (> r1 (* r1 r0 83.0 83.0) r2 r3 r3)) v52)))
(assert (or (and (and v12 v11 (>= 307769.0 r5) v40 (>= r6 (/ r0 (/ 83.0 r2)) (+ r1 r3 (* r1 r0 83.0 83.0) r2 r0) (* (- (* 26664.0 (* r1 r0 83.0 83.0) (/ r0 (/ 83.0 r2)) r1 (* r1 (* r1 r0 83.0 83.0) r1 r1)) 26664.0 83.0) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (<= (* (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)) r2 (* r1 (* r1 r0 83.0 83.0) r1 r1) (* r1 (* r1 r0 83.0 83.0) r1 r1) 6618424257.0) 2.0 (* (/ r0 (/ 83.0 r2)) 2.0 r6 (* r1 r0 83.0 83.0))) (<= (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1))) (/ r8 6618424257.0)) v30) (and (= (* r1 r0 83.0 83.0) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)) r1) (>= 83.0 r2 (* r1 (* r1 r0 83.0 83.0) r1 r1) r1 83.0) v1 v10 v18 (> r1 (* r1 r0 83.0 83.0) r2 r3 r3)) v52) (distinct (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1))))) v44))
(assert (or v26 v5 (<= 26664.0 (- r1))))
(assert (or v39 (distinct (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1))))) v38))
(assert (or v30 (<= (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (+ (- (* 26664.0 (* r1 r0 83.0 83.0) (/ r0 (/ 83.0 r2)) r1 (* r1 (* r1 r0 83.0 83.0) r1 r1)) 26664.0 83.0) (/ r8 6618424257.0) r2 26664.0) (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (/ r5 (/ (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (* 26664.0 (* r1 r0 83.0 83.0) (/ r0 (/ 83.0 r2)) r1 (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (* (- r2) (* r1 r0 83.0 83.0) r2 (/ 83.0 r2))) (<= 26664.0 (- r1))))
(assert (or (<= 26664.0 (- (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3))) (<= 26664.0 (- r1)) v39))
(assert (or (= (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)) (* (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)) r2 (* r1 (* r1 r0 83.0 83.0) r1 r1) (* r1 (* r1 r0 83.0 83.0) r1 r1) 6618424257.0) r2 (/ 83.0 (- r2)) (* (- (* 26664.0 (* r1 r0 83.0 83.0) (/ r0 (/ 83.0 r2)) r1 (* r1 (* r1 r0 83.0 83.0) r1 r1)) 26664.0 83.0) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (= (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)) (* (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)) r2 (* r1 (* r1 r0 83.0 83.0) r1 r1) (* r1 (* r1 r0 83.0 83.0) r1 r1) 6618424257.0) r2 (/ 83.0 (- r2)) (* (- (* 26664.0 (* r1 r0 83.0 83.0) (/ r0 (/ 83.0 r2)) r1 (* r1 (* r1 r0 83.0 83.0) r1 r1)) 26664.0 83.0) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) v5))
(assert (or (and (and v12 v11 (>= 307769.0 r5) v40 (>= r6 (/ r0 (/ 83.0 r2)) (+ r1 r3 (* r1 r0 83.0 83.0) r2 r0) (* (- (* 26664.0 (* r1 r0 83.0 83.0) (/ r0 (/ 83.0 r2)) r1 (* r1 (* r1 r0 83.0 83.0) r1 r1)) 26664.0 83.0) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (<= (* (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)) r2 (* r1 (* r1 r0 83.0 83.0) r1 r1) (* r1 (* r1 r0 83.0 83.0) r1 r1) 6618424257.0) 2.0 (* (/ r0 (/ 83.0 r2)) 2.0 r6 (* r1 r0 83.0 83.0))) (<= (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1))) (/ r8 6618424257.0)) v30) (and (= (* r1 r0 83.0 83.0) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)) r1) (>= 83.0 r2 (* r1 (* r1 r0 83.0 83.0) r1 r1) r1 83.0) v1 v10 v18 (> r1 (* r1 r0 83.0 83.0) r2 r3 r3)) v52) v26 (>= (/ r2 (* (/ r0 (/ 83.0 r2)) 2.0 r6 (* r1 r0 83.0 83.0))) r4 (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (/ (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (* 26664.0 (* r1 r0 83.0 83.0) (/ r0 (/ 83.0 r2)) r1 (* r1 (* r1 r0 83.0 83.0) r1 r1))))))
(assert (or v60 (<= 26664.0 (- r1)) (and (and v12 v11 (>= 307769.0 r5) v40 (>= r6 (/ r0 (/ 83.0 r2)) (+ r1 r3 (* r1 r0 83.0 83.0) r2 r0) (* (- (* 26664.0 (* r1 r0 83.0 83.0) (/ r0 (/ 83.0 r2)) r1 (* r1 (* r1 r0 83.0 83.0) r1 r1)) 26664.0 83.0) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (<= (* (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)) r2 (* r1 (* r1 r0 83.0 83.0) r1 r1) (* r1 (* r1 r0 83.0 83.0) r1 r1) 6618424257.0) 2.0 (* (/ r0 (/ 83.0 r2)) 2.0 r6 (* r1 r0 83.0 83.0))) (<= (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1))) (/ r8 6618424257.0)) v30) (and (= (* r1 r0 83.0 83.0) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)) r1) (>= 83.0 r2 (* r1 (* r1 r0 83.0 83.0) r1 r1) r1 83.0) v1 v10 v18 (> r1 (* r1 r0 83.0 83.0) r2 r3 r3)) v52)))
(assert (or (<= 26664.0 (- r1)) (>= (/ r2 (* (/ r0 (/ 83.0 r2)) 2.0 r6 (* r1 r0 83.0 83.0))) r4 (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (/ (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (* 26664.0 (* r1 r0 83.0 83.0) (/ r0 (/ 83.0 r2)) r1 (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (< (- (* r1 r0 83.0 83.0)) (/ r8 6618424257.0))))
(assert (or v5 (xor (>= (* r1 (* r1 r0 83.0 83.0) r1 r1) 2426.0 2426.0 6618424257.0) v59 v7) (<= (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (+ (- (* 26664.0 (* r1 r0 83.0 83.0) (/ r0 (/ 83.0 r2)) r1 (* r1 (* r1 r0 83.0 83.0) r1 r1)) 26664.0 83.0) (/ r8 6618424257.0) r2 26664.0) (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (/ r5 (/ (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (* 26664.0 (* r1 r0 83.0 83.0) (/ r0 (/ 83.0 r2)) r1 (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (* (- r2) (* r1 r0 83.0 83.0) r2 (/ 83.0 r2)))))
(assert (or (<= (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (+ (- (* 26664.0 (* r1 r0 83.0 83.0) (/ r0 (/ 83.0 r2)) r1 (* r1 (* r1 r0 83.0 83.0) r1 r1)) 26664.0 83.0) (/ r8 6618424257.0) r2 26664.0) (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (/ r5 (/ (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (* 26664.0 (* r1 r0 83.0 83.0) (/ r0 (/ 83.0 r2)) r1 (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (* (- r2) (* r1 r0 83.0 83.0) r2 (/ 83.0 r2))) (xor (>= (* r1 (* r1 r0 83.0 83.0) r1 r1) 2426.0 2426.0 6618424257.0) v59 v7) (<= 26664.0 (- r1))))
(assert (or v39 (and (and v12 v11 (>= 307769.0 r5) v40 (>= r6 (/ r0 (/ 83.0 r2)) (+ r1 r3 (* r1 r0 83.0 83.0) r2 r0) (* (- (* 26664.0 (* r1 r0 83.0 83.0) (/ r0 (/ 83.0 r2)) r1 (* r1 (* r1 r0 83.0 83.0) r1 r1)) 26664.0 83.0) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (<= (* (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)) r2 (* r1 (* r1 r0 83.0 83.0) r1 r1) (* r1 (* r1 r0 83.0 83.0) r1 r1) 6618424257.0) 2.0 (* (/ r0 (/ 83.0 r2)) 2.0 r6 (* r1 r0 83.0 83.0))) (<= (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1))) (/ r8 6618424257.0)) v30) (and (= (* r1 r0 83.0 83.0) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)) r1) (>= 83.0 r2 (* r1 (* r1 r0 83.0 83.0) r1 r1) r1 83.0) v1 v10 v18 (> r1 (* r1 r0 83.0 83.0) r2 r3 r3)) v52) v26))
(assert (or v38 v5 (<= 26664.0 (- r1))))
(assert (or (distinct (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1))))) v5 (<= 26664.0 (- r1))))
(assert (or v26 v5 v26))
(assert (or (>= (/ r2 (* (/ r0 (/ 83.0 r2)) 2.0 r6 (* r1 r0 83.0 83.0))) r4 (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (/ (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (* 26664.0 (* r1 r0 83.0 83.0) (/ r0 (/ 83.0 r2)) r1 (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (<= (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (+ (- (* 26664.0 (* r1 r0 83.0 83.0) (/ r0 (/ 83.0 r2)) r1 (* r1 (* r1 r0 83.0 83.0) r1 r1)) 26664.0 83.0) (/ r8 6618424257.0) r2 26664.0) (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (/ r5 (/ (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (* 26664.0 (* r1 r0 83.0 83.0) (/ r0 (/ 83.0 r2)) r1 (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (* (- r2) (* r1 r0 83.0 83.0) r2 (/ 83.0 r2))) (<= (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (+ (- (* 26664.0 (* r1 r0 83.0 83.0) (/ r0 (/ 83.0 r2)) r1 (* r1 (* r1 r0 83.0 83.0) r1 r1)) 26664.0 83.0) (/ r8 6618424257.0) r2 26664.0) (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (/ r5 (/ (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (* 26664.0 (* r1 r0 83.0 83.0) (/ r0 (/ 83.0 r2)) r1 (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (* (- r2) (* r1 r0 83.0 83.0) r2 (/ 83.0 r2)))))
(assert (or (and (and v12 v11 (>= 307769.0 r5) v40 (>= r6 (/ r0 (/ 83.0 r2)) (+ r1 r3 (* r1 r0 83.0 83.0) r2 r0) (* (- (* 26664.0 (* r1 r0 83.0 83.0) (/ r0 (/ 83.0 r2)) r1 (* r1 (* r1 r0 83.0 83.0) r1 r1)) 26664.0 83.0) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (<= (* (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)) r2 (* r1 (* r1 r0 83.0 83.0) r1 r1) (* r1 (* r1 r0 83.0 83.0) r1 r1) 6618424257.0) 2.0 (* (/ r0 (/ 83.0 r2)) 2.0 r6 (* r1 r0 83.0 83.0))) (<= (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1))) (/ r8 6618424257.0)) v30) (and (= (* r1 r0 83.0 83.0) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)) r1) (>= 83.0 r2 (* r1 (* r1 r0 83.0 83.0) r1 r1) r1 83.0) v1 v10 v18 (> r1 (* r1 r0 83.0 83.0) r2 r3 r3)) v52) (<= 26664.0 (- r1)) v39))
(assert (or v39 (= (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)) (* (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)) r2 (* r1 (* r1 r0 83.0 83.0) r1 r1) (* r1 (* r1 r0 83.0 83.0) r1 r1) 6618424257.0) r2 (/ 83.0 (- r2)) (* (- (* 26664.0 (* r1 r0 83.0 83.0) (/ r0 (/ 83.0 r2)) r1 (* r1 (* r1 r0 83.0 83.0) r1 r1)) 26664.0 83.0) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (< (- (* r1 r0 83.0 83.0)) (/ r8 6618424257.0))))
(assert (or v44 (= (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)) (* (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)) r2 (* r1 (* r1 r0 83.0 83.0) r1 r1) (* r1 (* r1 r0 83.0 83.0) r1 r1) 6618424257.0) r2 (/ 83.0 (- r2)) (* (- (* 26664.0 (* r1 r0 83.0 83.0) (/ r0 (/ 83.0 r2)) r1 (* r1 (* r1 r0 83.0 83.0) r1 r1)) 26664.0 83.0) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (xor (>= (* r1 (* r1 r0 83.0 83.0) r1 r1) 2426.0 2426.0 6618424257.0) v59 v7)))
(assert (or (= (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)) (* (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)) r2 (* r1 (* r1 r0 83.0 83.0) r1 r1) (* r1 (* r1 r0 83.0 83.0) r1 r1) 6618424257.0) r2 (/ 83.0 (- r2)) (* (- (* 26664.0 (* r1 r0 83.0 83.0) (/ r0 (/ 83.0 r2)) r1 (* r1 (* r1 r0 83.0 83.0) r1 r1)) 26664.0 83.0) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (<= 26664.0 (- (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3))) (distinct (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))))))
(assert (or (<= (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (+ (- (* 26664.0 (* r1 r0 83.0 83.0) (/ r0 (/ 83.0 r2)) r1 (* r1 (* r1 r0 83.0 83.0) r1 r1)) 26664.0 83.0) (/ r8 6618424257.0) r2 26664.0) (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (/ r5 (/ (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (* 26664.0 (* r1 r0 83.0 83.0) (/ r0 (/ 83.0 r2)) r1 (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (* (- r2) (* r1 r0 83.0 83.0) r2 (/ 83.0 r2))) v38 v38))
(assert (or v38 (<= 26664.0 (- r1)) v38))
(assert (or v26 (= (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)) (* (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)) r2 (* r1 (* r1 r0 83.0 83.0) r1 r1) (* r1 (* r1 r0 83.0 83.0) r1 r1) 6618424257.0) r2 (/ 83.0 (- r2)) (* (- (* 26664.0 (* r1 r0 83.0 83.0) (/ r0 (/ 83.0 r2)) r1 (* r1 (* r1 r0 83.0 83.0) r1 r1)) 26664.0 83.0) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) v5))
(assert (or v30 v39 (<= 26664.0 (- (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3)))))
(assert (or v60 v5 v5))
(assert (or v5 v39 (and (and v12 v11 (>= 307769.0 r5) v40 (>= r6 (/ r0 (/ 83.0 r2)) (+ r1 r3 (* r1 r0 83.0 83.0) r2 r0) (* (- (* 26664.0 (* r1 r0 83.0 83.0) (/ r0 (/ 83.0 r2)) r1 (* r1 (* r1 r0 83.0 83.0) r1 r1)) 26664.0 83.0) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (<= (* (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)) r2 (* r1 (* r1 r0 83.0 83.0) r1 r1) (* r1 (* r1 r0 83.0 83.0) r1 r1) 6618424257.0) 2.0 (* (/ r0 (/ 83.0 r2)) 2.0 r6 (* r1 r0 83.0 83.0))) (<= (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1))) (/ r8 6618424257.0)) v30) (and (= (* r1 r0 83.0 83.0) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)) r1) (>= 83.0 r2 (* r1 (* r1 r0 83.0 83.0) r1 r1) r1 83.0) v1 v10 v18 (> r1 (* r1 r0 83.0 83.0) r2 r3 r3)) v52)))
(assert (or (xor (>= (* r1 (* r1 r0 83.0 83.0) r1 r1) 2426.0 2426.0 6618424257.0) v59 v7) (xor (>= (* r1 (* r1 r0 83.0 83.0) r1 r1) 2426.0 2426.0 6618424257.0) v59 v7) (>= (/ r2 (* (/ r0 (/ 83.0 r2)) 2.0 r6 (* r1 r0 83.0 83.0))) r4 (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (/ (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (* 26664.0 (* r1 r0 83.0 83.0) (/ r0 (/ 83.0 r2)) r1 (* r1 (* r1 r0 83.0 83.0) r1 r1))))))
(assert (or (<= 26664.0 (- (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3))) (and (and v12 v11 (>= 307769.0 r5) v40 (>= r6 (/ r0 (/ 83.0 r2)) (+ r1 r3 (* r1 r0 83.0 83.0) r2 r0) (* (- (* 26664.0 (* r1 r0 83.0 83.0) (/ r0 (/ 83.0 r2)) r1 (* r1 (* r1 r0 83.0 83.0) r1 r1)) 26664.0 83.0) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (<= (* (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)) r2 (* r1 (* r1 r0 83.0 83.0) r1 r1) (* r1 (* r1 r0 83.0 83.0) r1 r1) 6618424257.0) 2.0 (* (/ r0 (/ 83.0 r2)) 2.0 r6 (* r1 r0 83.0 83.0))) (<= (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1))) (/ r8 6618424257.0)) v30) (and (= (* r1 r0 83.0 83.0) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)) r1) (>= 83.0 r2 (* r1 (* r1 r0 83.0 83.0) r1 r1) r1 83.0) v1 v10 v18 (> r1 (* r1 r0 83.0 83.0) r2 r3 r3)) v52) v60))
(assert (or (<= (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (+ (- (* 26664.0 (* r1 r0 83.0 83.0) (/ r0 (/ 83.0 r2)) r1 (* r1 (* r1 r0 83.0 83.0) r1 r1)) 26664.0 83.0) (/ r8 6618424257.0) r2 26664.0) (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (/ r5 (/ (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (* 26664.0 (* r1 r0 83.0 83.0) (/ r0 (/ 83.0 r2)) r1 (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (* (- r2) (* r1 r0 83.0 83.0) r2 (/ 83.0 r2))) v30 (>= (/ r2 (* (/ r0 (/ 83.0 r2)) 2.0 r6 (* r1 r0 83.0 83.0))) r4 (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (/ (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (* 26664.0 (* r1 r0 83.0 83.0) (/ r0 (/ 83.0 r2)) r1 (* r1 (* r1 r0 83.0 83.0) r1 r1))))))
(assert (or (<= 26664.0 (- (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3))) (distinct (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1))))) (distinct (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))))))
(assert (or v26 (= (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)) (* (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)) r2 (* r1 (* r1 r0 83.0 83.0) r1 r1) (* r1 (* r1 r0 83.0 83.0) r1 r1) 6618424257.0) r2 (/ 83.0 (- r2)) (* (- (* 26664.0 (* r1 r0 83.0 83.0) (/ r0 (/ 83.0 r2)) r1 (* r1 (* r1 r0 83.0 83.0) r1 r1)) 26664.0 83.0) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (<= (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (+ (- (* 26664.0 (* r1 r0 83.0 83.0) (/ r0 (/ 83.0 r2)) r1 (* r1 (* r1 r0 83.0 83.0) r1 r1)) 26664.0 83.0) (/ r8 6618424257.0) r2 26664.0) (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (/ r5 (/ (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (* 26664.0 (* r1 r0 83.0 83.0) (/ r0 (/ 83.0 r2)) r1 (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (* (- r2) (* r1 r0 83.0 83.0) r2 (/ 83.0 r2)))))
(assert (or v30 v5 v39))
(assert (or v60 (= (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)) (* (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)) r2 (* r1 (* r1 r0 83.0 83.0) r1 r1) (* r1 (* r1 r0 83.0 83.0) r1 r1) 6618424257.0) r2 (/ 83.0 (- r2)) (* (- (* 26664.0 (* r1 r0 83.0 83.0) (/ r0 (/ 83.0 r2)) r1 (* r1 (* r1 r0 83.0 83.0) r1 r1)) 26664.0 83.0) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) v38))
(assert (or v60 v60 (distinct (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))))))
(assert (or (and (and v12 v11 (>= 307769.0 r5) v40 (>= r6 (/ r0 (/ 83.0 r2)) (+ r1 r3 (* r1 r0 83.0 83.0) r2 r0) (* (- (* 26664.0 (* r1 r0 83.0 83.0) (/ r0 (/ 83.0 r2)) r1 (* r1 (* r1 r0 83.0 83.0) r1 r1)) 26664.0 83.0) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (<= (* (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)) r2 (* r1 (* r1 r0 83.0 83.0) r1 r1) (* r1 (* r1 r0 83.0 83.0) r1 r1) 6618424257.0) 2.0 (* (/ r0 (/ 83.0 r2)) 2.0 r6 (* r1 r0 83.0 83.0))) (<= (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1))) (/ r8 6618424257.0)) v30) (and (= (* r1 r0 83.0 83.0) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)) r1) (>= 83.0 r2 (* r1 (* r1 r0 83.0 83.0) r1 r1) r1 83.0) v1 v10 v18 (> r1 (* r1 r0 83.0 83.0) r2 r3 r3)) v52) v26 (distinct (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))))))
(assert (or (>= (/ r2 (* (/ r0 (/ 83.0 r2)) 2.0 r6 (* r1 r0 83.0 83.0))) r4 (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (/ (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (* 26664.0 (* r1 r0 83.0 83.0) (/ r0 (/ 83.0 r2)) r1 (* r1 (* r1 r0 83.0 83.0) r1 r1)))) v26 (distinct (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))))))
(assert (or v44 v39 (<= (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (+ (- (* 26664.0 (* r1 r0 83.0 83.0) (/ r0 (/ 83.0 r2)) r1 (* r1 (* r1 r0 83.0 83.0) r1 r1)) 26664.0 83.0) (/ r8 6618424257.0) r2 26664.0) (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (/ r5 (/ (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (* 26664.0 (* r1 r0 83.0 83.0) (/ r0 (/ 83.0 r2)) r1 (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (* (- r2) (* r1 r0 83.0 83.0) r2 (/ 83.0 r2)))))
(assert (or v30 (>= (/ r2 (* (/ r0 (/ 83.0 r2)) 2.0 r6 (* r1 r0 83.0 83.0))) r4 (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (/ (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (* 26664.0 (* r1 r0 83.0 83.0) (/ r0 (/ 83.0 r2)) r1 (* r1 (* r1 r0 83.0 83.0) r1 r1)))) v60))
(assert (or v44 (<= (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (+ (- (* 26664.0 (* r1 r0 83.0 83.0) (/ r0 (/ 83.0 r2)) r1 (* r1 (* r1 r0 83.0 83.0) r1 r1)) 26664.0 83.0) (/ r8 6618424257.0) r2 26664.0) (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (/ r5 (/ (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (* 26664.0 (* r1 r0 83.0 83.0) (/ r0 (/ 83.0 r2)) r1 (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (* (- r2) (* r1 r0 83.0 83.0) r2 (/ 83.0 r2))) (and (and v12 v11 (>= 307769.0 r5) v40 (>= r6 (/ r0 (/ 83.0 r2)) (+ r1 r3 (* r1 r0 83.0 83.0) r2 r0) (* (- (* 26664.0 (* r1 r0 83.0 83.0) (/ r0 (/ 83.0 r2)) r1 (* r1 (* r1 r0 83.0 83.0) r1 r1)) 26664.0 83.0) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (<= (* (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)) r2 (* r1 (* r1 r0 83.0 83.0) r1 r1) (* r1 (* r1 r0 83.0 83.0) r1 r1) 6618424257.0) 2.0 (* (/ r0 (/ 83.0 r2)) 2.0 r6 (* r1 r0 83.0 83.0))) (<= (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1))) (/ r8 6618424257.0)) v30) (and (= (* r1 r0 83.0 83.0) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)) r1) (>= 83.0 r2 (* r1 (* r1 r0 83.0 83.0) r1 r1) r1 83.0) v1 v10 v18 (> r1 (* r1 r0 83.0 83.0) r2 r3 r3)) v52)))
(assert (or (and (and v12 v11 (>= 307769.0 r5) v40 (>= r6 (/ r0 (/ 83.0 r2)) (+ r1 r3 (* r1 r0 83.0 83.0) r2 r0) (* (- (* 26664.0 (* r1 r0 83.0 83.0) (/ r0 (/ 83.0 r2)) r1 (* r1 (* r1 r0 83.0 83.0) r1 r1)) 26664.0 83.0) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (<= (* (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)) r2 (* r1 (* r1 r0 83.0 83.0) r1 r1) (* r1 (* r1 r0 83.0 83.0) r1 r1) 6618424257.0) 2.0 (* (/ r0 (/ 83.0 r2)) 2.0 r6 (* r1 r0 83.0 83.0))) (<= (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1))) (/ r8 6618424257.0)) v30) (and (= (* r1 r0 83.0 83.0) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)) r1) (>= 83.0 r2 (* r1 (* r1 r0 83.0 83.0) r1 r1) r1 83.0) v1 v10 v18 (> r1 (* r1 r0 83.0 83.0) r2 r3 r3)) v52) (<= (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (+ (- (* 26664.0 (* r1 r0 83.0 83.0) (/ r0 (/ 83.0 r2)) r1 (* r1 (* r1 r0 83.0 83.0) r1 r1)) 26664.0 83.0) (/ r8 6618424257.0) r2 26664.0) (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (/ r5 (/ (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (* 26664.0 (* r1 r0 83.0 83.0) (/ r0 (/ 83.0 r2)) r1 (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (* (- r2) (* r1 r0 83.0 83.0) r2 (/ 83.0 r2))) (xor (>= (* r1 (* r1 r0 83.0 83.0) r1 r1) 2426.0 2426.0 6618424257.0) v59 v7)))
(assert (or (xor (>= (* r1 (* r1 r0 83.0 83.0) r1 r1) 2426.0 2426.0 6618424257.0) v59 v7) v5 (= (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)) (* (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)) r2 (* r1 (* r1 r0 83.0 83.0) r1 r1) (* r1 (* r1 r0 83.0 83.0) r1 r1) 6618424257.0) r2 (/ 83.0 (- r2)) (* (- (* 26664.0 (* r1 r0 83.0 83.0) (/ r0 (/ 83.0 r2)) r1 (* r1 (* r1 r0 83.0 83.0) r1 r1)) 26664.0 83.0) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1))))))
(assert (or v30 (<= (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (+ (- (* 26664.0 (* r1 r0 83.0 83.0) (/ r0 (/ 83.0 r2)) r1 (* r1 (* r1 r0 83.0 83.0) r1 r1)) 26664.0 83.0) (/ r8 6618424257.0) r2 26664.0) (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (/ r5 (/ (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (* 26664.0 (* r1 r0 83.0 83.0) (/ r0 (/ 83.0 r2)) r1 (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (* (- r2) (* r1 r0 83.0 83.0) r2 (/ 83.0 r2))) (= (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)) (* (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)) r2 (* r1 (* r1 r0 83.0 83.0) r1 r1) (* r1 (* r1 r0 83.0 83.0) r1 r1) 6618424257.0) r2 (/ 83.0 (- r2)) (* (- (* 26664.0 (* r1 r0 83.0 83.0) (/ r0 (/ 83.0 r2)) r1 (* r1 (* r1 r0 83.0 83.0) r1 r1)) 26664.0 83.0) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1))))))
(assert (or v39 (<= 26664.0 (- r1)) v39))
(assert (or v39 (= (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)) (* (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)) r2 (* r1 (* r1 r0 83.0 83.0) r1 r1) (* r1 (* r1 r0 83.0 83.0) r1 r1) 6618424257.0) r2 (/ 83.0 (- r2)) (* (- (* 26664.0 (* r1 r0 83.0 83.0) (/ r0 (/ 83.0 r2)) r1 (* r1 (* r1 r0 83.0 83.0) r1 r1)) 26664.0 83.0) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (xor (>= (* r1 (* r1 r0 83.0 83.0) r1 r1) 2426.0 2426.0 6618424257.0) v59 v7)))
(assert (or v26 v30 (= (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)) (* (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)) r2 (* r1 (* r1 r0 83.0 83.0) r1 r1) (* r1 (* r1 r0 83.0 83.0) r1 r1) 6618424257.0) r2 (/ 83.0 (- r2)) (* (- (* 26664.0 (* r1 r0 83.0 83.0) (/ r0 (/ 83.0 r2)) r1 (* r1 (* r1 r0 83.0 83.0) r1 r1)) 26664.0 83.0) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1))))))
(assert (or (xor (>= (* r1 (* r1 r0 83.0 83.0) r1 r1) 2426.0 2426.0 6618424257.0) v59 v7) v38 (<= 26664.0 (- (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3)))))
(assert (or v44 (< (- (* r1 r0 83.0 83.0)) (/ r8 6618424257.0)) (<= 26664.0 (- (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3)))))
(assert (or v44 v60 v30))
(assert (or (<= (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (+ (- (* 26664.0 (* r1 r0 83.0 83.0) (/ r0 (/ 83.0 r2)) r1 (* r1 (* r1 r0 83.0 83.0) r1 r1)) 26664.0 83.0) (/ r8 6618424257.0) r2 26664.0) (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (/ r5 (/ (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (* 26664.0 (* r1 r0 83.0 83.0) (/ r0 (/ 83.0 r2)) r1 (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (* (- r2) (* r1 r0 83.0 83.0) r2 (/ 83.0 r2))) (< (- (* r1 r0 83.0 83.0)) (/ r8 6618424257.0)) v5))
(assert (or v30 (distinct (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1))))) (and (and v12 v11 (>= 307769.0 r5) v40 (>= r6 (/ r0 (/ 83.0 r2)) (+ r1 r3 (* r1 r0 83.0 83.0) r2 r0) (* (- (* 26664.0 (* r1 r0 83.0 83.0) (/ r0 (/ 83.0 r2)) r1 (* r1 (* r1 r0 83.0 83.0) r1 r1)) 26664.0 83.0) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (<= (* (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)) r2 (* r1 (* r1 r0 83.0 83.0) r1 r1) (* r1 (* r1 r0 83.0 83.0) r1 r1) 6618424257.0) 2.0 (* (/ r0 (/ 83.0 r2)) 2.0 r6 (* r1 r0 83.0 83.0))) (<= (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1))) (/ r8 6618424257.0)) v30) (and (= (* r1 r0 83.0 83.0) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)) r1) (>= 83.0 r2 (* r1 (* r1 r0 83.0 83.0) r1 r1) r1 83.0) v1 v10 v18 (> r1 (* r1 r0 83.0 83.0) r2 r3 r3)) v52)))
(assert (or v44 v30 v44))
(assert (or (<= 26664.0 (- (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3))) (distinct (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1))))) (< (- (* r1 r0 83.0 83.0)) (/ r8 6618424257.0))))
(assert (or v38 (<= 26664.0 (- r1)) v5))
(assert (or (<= 26664.0 (- r1)) (<= (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (+ (- (* 26664.0 (* r1 r0 83.0 83.0) (/ r0 (/ 83.0 r2)) r1 (* r1 (* r1 r0 83.0 83.0) r1 r1)) 26664.0 83.0) (/ r8 6618424257.0) r2 26664.0) (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (/ r5 (/ (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (* 26664.0 (* r1 r0 83.0 83.0) (/ r0 (/ 83.0 r2)) r1 (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (* (- r2) (* r1 r0 83.0 83.0) r2 (/ 83.0 r2))) (<= (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (+ (- (* 26664.0 (* r1 r0 83.0 83.0) (/ r0 (/ 83.0 r2)) r1 (* r1 (* r1 r0 83.0 83.0) r1 r1)) 26664.0 83.0) (/ r8 6618424257.0) r2 26664.0) (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (/ r5 (/ (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (* 26664.0 (* r1 r0 83.0 83.0) (/ r0 (/ 83.0 r2)) r1 (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (* (- r2) (* r1 r0 83.0 83.0) r2 (/ 83.0 r2)))))
(assert (or (<= (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (+ (- (* 26664.0 (* r1 r0 83.0 83.0) (/ r0 (/ 83.0 r2)) r1 (* r1 (* r1 r0 83.0 83.0) r1 r1)) 26664.0 83.0) (/ r8 6618424257.0) r2 26664.0) (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (/ r5 (/ (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (* 26664.0 (* r1 r0 83.0 83.0) (/ r0 (/ 83.0 r2)) r1 (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (* (- r2) (* r1 r0 83.0 83.0) r2 (/ 83.0 r2))) (<= (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (+ (- (* 26664.0 (* r1 r0 83.0 83.0) (/ r0 (/ 83.0 r2)) r1 (* r1 (* r1 r0 83.0 83.0) r1 r1)) 26664.0 83.0) (/ r8 6618424257.0) r2 26664.0) (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (/ r5 (/ (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (* 26664.0 (* r1 r0 83.0 83.0) (/ r0 (/ 83.0 r2)) r1 (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (* (- r2) (* r1 r0 83.0 83.0) r2 (/ 83.0 r2))) v5))
(assert (or (= (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)) (* (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)) r2 (* r1 (* r1 r0 83.0 83.0) r1 r1) (* r1 (* r1 r0 83.0 83.0) r1 r1) 6618424257.0) r2 (/ 83.0 (- r2)) (* (- (* 26664.0 (* r1 r0 83.0 83.0) (/ r0 (/ 83.0 r2)) r1 (* r1 (* r1 r0 83.0 83.0) r1 r1)) 26664.0 83.0) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (>= (/ r2 (* (/ r0 (/ 83.0 r2)) 2.0 r6 (* r1 r0 83.0 83.0))) r4 (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (/ (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (* 26664.0 (* r1 r0 83.0 83.0) (/ r0 (/ 83.0 r2)) r1 (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (>= (/ r2 (* (/ r0 (/ 83.0 r2)) 2.0 r6 (* r1 r0 83.0 83.0))) r4 (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (/ (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (* 26664.0 (* r1 r0 83.0 83.0) (/ r0 (/ 83.0 r2)) r1 (* r1 (* r1 r0 83.0 83.0) r1 r1))))))
(assert (or v30 v5 (< (- (* r1 r0 83.0 83.0)) (/ r8 6618424257.0))))
(assert (or (<= (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (+ (- (* 26664.0 (* r1 r0 83.0 83.0) (/ r0 (/ 83.0 r2)) r1 (* r1 (* r1 r0 83.0 83.0) r1 r1)) 26664.0 83.0) (/ r8 6618424257.0) r2 26664.0) (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (/ r5 (/ (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (* 26664.0 (* r1 r0 83.0 83.0) (/ r0 (/ 83.0 r2)) r1 (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (* (- r2) (* r1 r0 83.0 83.0) r2 (/ 83.0 r2))) v39 (= (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)) (* (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)) r2 (* r1 (* r1 r0 83.0 83.0) r1 r1) (* r1 (* r1 r0 83.0 83.0) r1 r1) 6618424257.0) r2 (/ 83.0 (- r2)) (* (- (* 26664.0 (* r1 r0 83.0 83.0) (/ r0 (/ 83.0 r2)) r1 (* r1 (* r1 r0 83.0 83.0) r1 r1)) 26664.0 83.0) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1))))))
(assert (or v39 (xor (>= (* r1 (* r1 r0 83.0 83.0) r1 r1) 2426.0 2426.0 6618424257.0) v59 v7) (<= (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (+ (- (* 26664.0 (* r1 r0 83.0 83.0) (/ r0 (/ 83.0 r2)) r1 (* r1 (* r1 r0 83.0 83.0) r1 r1)) 26664.0 83.0) (/ r8 6618424257.0) r2 26664.0) (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (/ r5 (/ (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (* 26664.0 (* r1 r0 83.0 83.0) (/ r0 (/ 83.0 r2)) r1 (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (* (- r2) (* r1 r0 83.0 83.0) r2 (/ 83.0 r2)))))
(assert (or v44 v39 (>= (/ r2 (* (/ r0 (/ 83.0 r2)) 2.0 r6 (* r1 r0 83.0 83.0))) r4 (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (/ (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (* 26664.0 (* r1 r0 83.0 83.0) (/ r0 (/ 83.0 r2)) r1 (* r1 (* r1 r0 83.0 83.0) r1 r1))))))
(assert (or v5 v38 (<= 26664.0 (- (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3)))))
(assert (or (= (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)) (* (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)) r2 (* r1 (* r1 r0 83.0 83.0) r1 r1) (* r1 (* r1 r0 83.0 83.0) r1 r1) 6618424257.0) r2 (/ 83.0 (- r2)) (* (- (* 26664.0 (* r1 r0 83.0 83.0) (/ r0 (/ 83.0 r2)) r1 (* r1 (* r1 r0 83.0 83.0) r1 r1)) 26664.0 83.0) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (xor (>= (* r1 (* r1 r0 83.0 83.0) r1 r1) 2426.0 2426.0 6618424257.0) v59 v7) v44))
(assert (or v26 v44 v26))
(assert (or v5 (xor (>= (* r1 (* r1 r0 83.0 83.0) r1 r1) 2426.0 2426.0 6618424257.0) v59 v7) v5))
(assert (or (>= (/ r2 (* (/ r0 (/ 83.0 r2)) 2.0 r6 (* r1 r0 83.0 83.0))) r4 (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (/ (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (* 26664.0 (* r1 r0 83.0 83.0) (/ r0 (/ 83.0 r2)) r1 (* r1 (* r1 r0 83.0 83.0) r1 r1)))) v39 v26))
(assert (or (distinct (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1))))) v30 (< (- (* r1 r0 83.0 83.0)) (/ r8 6618424257.0))))
(assert (or (>= (/ r2 (* (/ r0 (/ 83.0 r2)) 2.0 r6 (* r1 r0 83.0 83.0))) r4 (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (/ (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (* 26664.0 (* r1 r0 83.0 83.0) (/ r0 (/ 83.0 r2)) r1 (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (and (and v12 v11 (>= 307769.0 r5) v40 (>= r6 (/ r0 (/ 83.0 r2)) (+ r1 r3 (* r1 r0 83.0 83.0) r2 r0) (* (- (* 26664.0 (* r1 r0 83.0 83.0) (/ r0 (/ 83.0 r2)) r1 (* r1 (* r1 r0 83.0 83.0) r1 r1)) 26664.0 83.0) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (<= (* (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)) r2 (* r1 (* r1 r0 83.0 83.0) r1 r1) (* r1 (* r1 r0 83.0 83.0) r1 r1) 6618424257.0) 2.0 (* (/ r0 (/ 83.0 r2)) 2.0 r6 (* r1 r0 83.0 83.0))) (<= (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1))) (/ r8 6618424257.0)) v30) (and (= (* r1 r0 83.0 83.0) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)) r1) (>= 83.0 r2 (* r1 (* r1 r0 83.0 83.0) r1 r1) r1 83.0) v1 v10 v18 (> r1 (* r1 r0 83.0 83.0) r2 r3 r3)) v52) (<= (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (+ (- (* 26664.0 (* r1 r0 83.0 83.0) (/ r0 (/ 83.0 r2)) r1 (* r1 (* r1 r0 83.0 83.0) r1 r1)) 26664.0 83.0) (/ r8 6618424257.0) r2 26664.0) (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (/ r5 (/ (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (* 26664.0 (* r1 r0 83.0 83.0) (/ r0 (/ 83.0 r2)) r1 (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (* (- r2) (* r1 r0 83.0 83.0) r2 (/ 83.0 r2)))))
(assert (or v30 (<= 26664.0 (- (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3))) (and (and v12 v11 (>= 307769.0 r5) v40 (>= r6 (/ r0 (/ 83.0 r2)) (+ r1 r3 (* r1 r0 83.0 83.0) r2 r0) (* (- (* 26664.0 (* r1 r0 83.0 83.0) (/ r0 (/ 83.0 r2)) r1 (* r1 (* r1 r0 83.0 83.0) r1 r1)) 26664.0 83.0) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (<= (* (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)) r2 (* r1 (* r1 r0 83.0 83.0) r1 r1) (* r1 (* r1 r0 83.0 83.0) r1 r1) 6618424257.0) 2.0 (* (/ r0 (/ 83.0 r2)) 2.0 r6 (* r1 r0 83.0 83.0))) (<= (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1))) (/ r8 6618424257.0)) v30) (and (= (* r1 r0 83.0 83.0) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)) r1) (>= 83.0 r2 (* r1 (* r1 r0 83.0 83.0) r1 r1) r1 83.0) v1 v10 v18 (> r1 (* r1 r0 83.0 83.0) r2 r3 r3)) v52)))
(assert (or (<= 26664.0 (- r1)) v5 v39))
(assert (or v60 (xor (>= (* r1 (* r1 r0 83.0 83.0) r1 r1) 2426.0 2426.0 6618424257.0) v59 v7) v30))
(assert (or v60 (distinct (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1))))) (distinct (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))))))
(assert (or (< (- (* r1 r0 83.0 83.0)) (/ r8 6618424257.0)) v39 (= (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)) (* (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)) r2 (* r1 (* r1 r0 83.0 83.0) r1 r1) (* r1 (* r1 r0 83.0 83.0) r1 r1) 6618424257.0) r2 (/ 83.0 (- r2)) (* (- (* 26664.0 (* r1 r0 83.0 83.0) (/ r0 (/ 83.0 r2)) r1 (* r1 (* r1 r0 83.0 83.0) r1 r1)) 26664.0 83.0) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1))))))
(assert (or (>= (/ r2 (* (/ r0 (/ 83.0 r2)) 2.0 r6 (* r1 r0 83.0 83.0))) r4 (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (/ (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (* 26664.0 (* r1 r0 83.0 83.0) (/ r0 (/ 83.0 r2)) r1 (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (< (- (* r1 r0 83.0 83.0)) (/ r8 6618424257.0)) v26))
(assert (or (= (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)) (* (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)) r2 (* r1 (* r1 r0 83.0 83.0) r1 r1) (* r1 (* r1 r0 83.0 83.0) r1 r1) 6618424257.0) r2 (/ 83.0 (- r2)) (* (- (* 26664.0 (* r1 r0 83.0 83.0) (/ r0 (/ 83.0 r2)) r1 (* r1 (* r1 r0 83.0 83.0) r1 r1)) 26664.0 83.0) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) v30 (>= (/ r2 (* (/ r0 (/ 83.0 r2)) 2.0 r6 (* r1 r0 83.0 83.0))) r4 (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (/ (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (* 26664.0 (* r1 r0 83.0 83.0) (/ r0 (/ 83.0 r2)) r1 (* r1 (* r1 r0 83.0 83.0) r1 r1))))))
(assert (or (= (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)) (* (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)) r2 (* r1 (* r1 r0 83.0 83.0) r1 r1) (* r1 (* r1 r0 83.0 83.0) r1 r1) 6618424257.0) r2 (/ 83.0 (- r2)) (* (- (* 26664.0 (* r1 r0 83.0 83.0) (/ r0 (/ 83.0 r2)) r1 (* r1 (* r1 r0 83.0 83.0) r1 r1)) 26664.0 83.0) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (and (and v12 v11 (>= 307769.0 r5) v40 (>= r6 (/ r0 (/ 83.0 r2)) (+ r1 r3 (* r1 r0 83.0 83.0) r2 r0) (* (- (* 26664.0 (* r1 r0 83.0 83.0) (/ r0 (/ 83.0 r2)) r1 (* r1 (* r1 r0 83.0 83.0) r1 r1)) 26664.0 83.0) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (<= (* (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)) r2 (* r1 (* r1 r0 83.0 83.0) r1 r1) (* r1 (* r1 r0 83.0 83.0) r1 r1) 6618424257.0) 2.0 (* (/ r0 (/ 83.0 r2)) 2.0 r6 (* r1 r0 83.0 83.0))) (<= (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1))) (/ r8 6618424257.0)) v30) (and (= (* r1 r0 83.0 83.0) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)) r1) (>= 83.0 r2 (* r1 (* r1 r0 83.0 83.0) r1 r1) r1 83.0) v1 v10 v18 (> r1 (* r1 r0 83.0 83.0) r2 r3 r3)) v52) (<= 26664.0 (- (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3)))))
(assert (or (< (- (* r1 r0 83.0 83.0)) (/ r8 6618424257.0)) (distinct (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1))))) v5))
(assert (or v5 v5 v44))
(assert (or (<= 26664.0 (- (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3))) v60 v39))
(assert (or v30 (<= 26664.0 (- r1)) (<= 26664.0 (- (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3)))))
(assert (or (and (and v12 v11 (>= 307769.0 r5) v40 (>= r6 (/ r0 (/ 83.0 r2)) (+ r1 r3 (* r1 r0 83.0 83.0) r2 r0) (* (- (* 26664.0 (* r1 r0 83.0 83.0) (/ r0 (/ 83.0 r2)) r1 (* r1 (* r1 r0 83.0 83.0) r1 r1)) 26664.0 83.0) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (<= (* (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)) r2 (* r1 (* r1 r0 83.0 83.0) r1 r1) (* r1 (* r1 r0 83.0 83.0) r1 r1) 6618424257.0) 2.0 (* (/ r0 (/ 83.0 r2)) 2.0 r6 (* r1 r0 83.0 83.0))) (<= (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1))) (/ r8 6618424257.0)) v30) (and (= (* r1 r0 83.0 83.0) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)) r1) (>= 83.0 r2 (* r1 (* r1 r0 83.0 83.0) r1 r1) r1 83.0) v1 v10 v18 (> r1 (* r1 r0 83.0 83.0) r2 r3 r3)) v52) (< (- (* r1 r0 83.0 83.0)) (/ r8 6618424257.0)) v38))
(assert (or (<= 26664.0 (- r1)) (= (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)) (* (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)) r2 (* r1 (* r1 r0 83.0 83.0) r1 r1) (* r1 (* r1 r0 83.0 83.0) r1 r1) 6618424257.0) r2 (/ 83.0 (- r2)) (* (- (* 26664.0 (* r1 r0 83.0 83.0) (/ r0 (/ 83.0 r2)) r1 (* r1 (* r1 r0 83.0 83.0) r1 r1)) 26664.0 83.0) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (and (and v12 v11 (>= 307769.0 r5) v40 (>= r6 (/ r0 (/ 83.0 r2)) (+ r1 r3 (* r1 r0 83.0 83.0) r2 r0) (* (- (* 26664.0 (* r1 r0 83.0 83.0) (/ r0 (/ 83.0 r2)) r1 (* r1 (* r1 r0 83.0 83.0) r1 r1)) 26664.0 83.0) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (<= (* (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)) r2 (* r1 (* r1 r0 83.0 83.0) r1 r1) (* r1 (* r1 r0 83.0 83.0) r1 r1) 6618424257.0) 2.0 (* (/ r0 (/ 83.0 r2)) 2.0 r6 (* r1 r0 83.0 83.0))) (<= (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1))) (/ r8 6618424257.0)) v30) (and (= (* r1 r0 83.0 83.0) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)) r1) (>= 83.0 r2 (* r1 (* r1 r0 83.0 83.0) r1 r1) r1 83.0) v1 v10 v18 (> r1 (* r1 r0 83.0 83.0) r2 r3 r3)) v52)))
(assert (or (xor (>= (* r1 (* r1 r0 83.0 83.0) r1 r1) 2426.0 2426.0 6618424257.0) v59 v7) (>= (/ r2 (* (/ r0 (/ 83.0 r2)) 2.0 r6 (* r1 r0 83.0 83.0))) r4 (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (/ (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (* 26664.0 (* r1 r0 83.0 83.0) (/ r0 (/ 83.0 r2)) r1 (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (< (- (* r1 r0 83.0 83.0)) (/ r8 6618424257.0))))
(assert (or (<= 26664.0 (- (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3))) (= (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)) (* (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)) r2 (* r1 (* r1 r0 83.0 83.0) r1 r1) (* r1 (* r1 r0 83.0 83.0) r1 r1) 6618424257.0) r2 (/ 83.0 (- r2)) (* (- (* 26664.0 (* r1 r0 83.0 83.0) (/ r0 (/ 83.0 r2)) r1 (* r1 (* r1 r0 83.0 83.0) r1 r1)) 26664.0 83.0) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (= (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)) (* (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)) r2 (* r1 (* r1 r0 83.0 83.0) r1 r1) (* r1 (* r1 r0 83.0 83.0) r1 r1) 6618424257.0) r2 (/ 83.0 (- r2)) (* (- (* 26664.0 (* r1 r0 83.0 83.0) (/ r0 (/ 83.0 r2)) r1 (* r1 (* r1 r0 83.0 83.0) r1 r1)) 26664.0 83.0) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1))))))
(assert (or v5 (>= (/ r2 (* (/ r0 (/ 83.0 r2)) 2.0 r6 (* r1 r0 83.0 83.0))) r4 (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (/ (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (* 26664.0 (* r1 r0 83.0 83.0) (/ r0 (/ 83.0 r2)) r1 (* r1 (* r1 r0 83.0 83.0) r1 r1)))) v26))
(assert (or (< (- (* r1 r0 83.0 83.0)) (/ r8 6618424257.0)) v44 (<= (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (+ (- (* 26664.0 (* r1 r0 83.0 83.0) (/ r0 (/ 83.0 r2)) r1 (* r1 (* r1 r0 83.0 83.0) r1 r1)) 26664.0 83.0) (/ r8 6618424257.0) r2 26664.0) (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (/ r5 (/ (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (* 26664.0 (* r1 r0 83.0 83.0) (/ r0 (/ 83.0 r2)) r1 (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (* (- r2) (* r1 r0 83.0 83.0) r2 (/ 83.0 r2)))))
(assert (or v39 v30 v39))
(assert (or v5 (>= (/ r2 (* (/ r0 (/ 83.0 r2)) 2.0 r6 (* r1 r0 83.0 83.0))) r4 (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (/ (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (* 26664.0 (* r1 r0 83.0 83.0) (/ r0 (/ 83.0 r2)) r1 (* r1 (* r1 r0 83.0 83.0) r1 r1)))) v44))
(assert (or (= (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)) (* (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)) r2 (* r1 (* r1 r0 83.0 83.0) r1 r1) (* r1 (* r1 r0 83.0 83.0) r1 r1) 6618424257.0) r2 (/ 83.0 (- r2)) (* (- (* 26664.0 (* r1 r0 83.0 83.0) (/ r0 (/ 83.0 r2)) r1 (* r1 (* r1 r0 83.0 83.0) r1 r1)) 26664.0 83.0) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (= (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)) (* (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)) r2 (* r1 (* r1 r0 83.0 83.0) r1 r1) (* r1 (* r1 r0 83.0 83.0) r1 r1) 6618424257.0) r2 (/ 83.0 (- r2)) (* (- (* 26664.0 (* r1 r0 83.0 83.0) (/ r0 (/ 83.0 r2)) r1 (* r1 (* r1 r0 83.0 83.0) r1 r1)) 26664.0 83.0) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) v39))
(assert (or (< (- (* r1 r0 83.0 83.0)) (/ r8 6618424257.0)) (distinct (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1))))) v39))
(assert (or (>= (/ r2 (* (/ r0 (/ 83.0 r2)) 2.0 r6 (* r1 r0 83.0 83.0))) r4 (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (/ (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (* 26664.0 (* r1 r0 83.0 83.0) (/ r0 (/ 83.0 r2)) r1 (* r1 (* r1 r0 83.0 83.0) r1 r1)))) v38 (< (- (* r1 r0 83.0 83.0)) (/ r8 6618424257.0))))
(assert (or (= (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)) (* (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)) r2 (* r1 (* r1 r0 83.0 83.0) r1 r1) (* r1 (* r1 r0 83.0 83.0) r1 r1) 6618424257.0) r2 (/ 83.0 (- r2)) (* (- (* 26664.0 (* r1 r0 83.0 83.0) (/ r0 (/ 83.0 r2)) r1 (* r1 (* r1 r0 83.0 83.0) r1 r1)) 26664.0 83.0) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (distinct (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1))))) v30))
(assert (or v5 (<= 26664.0 (- r1)) v5))
(assert (or v60 (distinct (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1))))) (<= 26664.0 (- (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3)))))
(assert (or (<= 26664.0 (- r1)) v39 (<= 26664.0 (- r1))))
(assert (or (= (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)) (* (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)) r2 (* r1 (* r1 r0 83.0 83.0) r1 r1) (* r1 (* r1 r0 83.0 83.0) r1 r1) 6618424257.0) r2 (/ 83.0 (- r2)) (* (- (* 26664.0 (* r1 r0 83.0 83.0) (/ r0 (/ 83.0 r2)) r1 (* r1 (* r1 r0 83.0 83.0) r1 r1)) 26664.0 83.0) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (xor (>= (* r1 (* r1 r0 83.0 83.0) r1 r1) 2426.0 2426.0 6618424257.0) v59 v7) v39))
(assert (or v60 (< (- (* r1 r0 83.0 83.0)) (/ r8 6618424257.0)) (<= (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (+ (- (* 26664.0 (* r1 r0 83.0 83.0) (/ r0 (/ 83.0 r2)) r1 (* r1 (* r1 r0 83.0 83.0) r1 r1)) 26664.0 83.0) (/ r8 6618424257.0) r2 26664.0) (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (/ r5 (/ (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (* 26664.0 (* r1 r0 83.0 83.0) (/ r0 (/ 83.0 r2)) r1 (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (* (- r2) (* r1 r0 83.0 83.0) r2 (/ 83.0 r2)))))
(assert (or (<= 26664.0 (- r1)) (<= (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (+ (- (* 26664.0 (* r1 r0 83.0 83.0) (/ r0 (/ 83.0 r2)) r1 (* r1 (* r1 r0 83.0 83.0) r1 r1)) 26664.0 83.0) (/ r8 6618424257.0) r2 26664.0) (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (/ r5 (/ (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (* 26664.0 (* r1 r0 83.0 83.0) (/ r0 (/ 83.0 r2)) r1 (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (* (- r2) (* r1 r0 83.0 83.0) r2 (/ 83.0 r2))) v5))
(assert (or v38 v38 v39))
(assert (or v26 (<= (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (+ (- (* 26664.0 (* r1 r0 83.0 83.0) (/ r0 (/ 83.0 r2)) r1 (* r1 (* r1 r0 83.0 83.0) r1 r1)) 26664.0 83.0) (/ r8 6618424257.0) r2 26664.0) (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (/ r5 (/ (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (* 26664.0 (* r1 r0 83.0 83.0) (/ r0 (/ 83.0 r2)) r1 (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (* (- r2) (* r1 r0 83.0 83.0) r2 (/ 83.0 r2))) (<= 26664.0 (- r1))))
(assert (or v38 v38 (distinct (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))))))
(assert (or v5 v39 (<= 26664.0 (- (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3)))))
(assert (or v5 (< (- (* r1 r0 83.0 83.0)) (/ r8 6618424257.0)) (< (- (* r1 r0 83.0 83.0)) (/ r8 6618424257.0))))
(assert (or (<= 26664.0 (- (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3))) (distinct (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1))))) (<= (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (+ (- (* 26664.0 (* r1 r0 83.0 83.0) (/ r0 (/ 83.0 r2)) r1 (* r1 (* r1 r0 83.0 83.0) r1 r1)) 26664.0 83.0) (/ r8 6618424257.0) r2 26664.0) (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (/ r5 (/ (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (* 26664.0 (* r1 r0 83.0 83.0) (/ r0 (/ 83.0 r2)) r1 (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (* (- r2) (* r1 r0 83.0 83.0) r2 (/ 83.0 r2)))))
(assert (or v60 v30 (< (- (* r1 r0 83.0 83.0)) (/ r8 6618424257.0))))
(assert (or v60 (<= 26664.0 (- (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3))) (= (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)) (* (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)) r2 (* r1 (* r1 r0 83.0 83.0) r1 r1) (* r1 (* r1 r0 83.0 83.0) r1 r1) 6618424257.0) r2 (/ 83.0 (- r2)) (* (- (* 26664.0 (* r1 r0 83.0 83.0) (/ r0 (/ 83.0 r2)) r1 (* r1 (* r1 r0 83.0 83.0) r1 r1)) 26664.0 83.0) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1))))))
(assert (or v39 (= (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)) (* (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)) r2 (* r1 (* r1 r0 83.0 83.0) r1 r1) (* r1 (* r1 r0 83.0 83.0) r1 r1) 6618424257.0) r2 (/ 83.0 (- r2)) (* (- (* 26664.0 (* r1 r0 83.0 83.0) (/ r0 (/ 83.0 r2)) r1 (* r1 (* r1 r0 83.0 83.0) r1 r1)) 26664.0 83.0) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (= (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)) (* (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)) r2 (* r1 (* r1 r0 83.0 83.0) r1 r1) (* r1 (* r1 r0 83.0 83.0) r1 r1) 6618424257.0) r2 (/ 83.0 (- r2)) (* (- (* 26664.0 (* r1 r0 83.0 83.0) (/ r0 (/ 83.0 r2)) r1 (* r1 (* r1 r0 83.0 83.0) r1 r1)) 26664.0 83.0) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1))))))
(assert (or v60 (= (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)) (* (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)) r2 (* r1 (* r1 r0 83.0 83.0) r1 r1) (* r1 (* r1 r0 83.0 83.0) r1 r1) 6618424257.0) r2 (/ 83.0 (- r2)) (* (- (* 26664.0 (* r1 r0 83.0 83.0) (/ r0 (/ 83.0 r2)) r1 (* r1 (* r1 r0 83.0 83.0) r1 r1)) 26664.0 83.0) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (<= 26664.0 (- (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3)))))
(assert (or v5 v26 (= (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)) (* (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)) r2 (* r1 (* r1 r0 83.0 83.0) r1 r1) (* r1 (* r1 r0 83.0 83.0) r1 r1) 6618424257.0) r2 (/ 83.0 (- r2)) (* (- (* 26664.0 (* r1 r0 83.0 83.0) (/ r0 (/ 83.0 r2)) r1 (* r1 (* r1 r0 83.0 83.0) r1 r1)) 26664.0 83.0) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1))))))
(assert (or (and (and v12 v11 (>= 307769.0 r5) v40 (>= r6 (/ r0 (/ 83.0 r2)) (+ r1 r3 (* r1 r0 83.0 83.0) r2 r0) (* (- (* 26664.0 (* r1 r0 83.0 83.0) (/ r0 (/ 83.0 r2)) r1 (* r1 (* r1 r0 83.0 83.0) r1 r1)) 26664.0 83.0) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (<= (* (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)) r2 (* r1 (* r1 r0 83.0 83.0) r1 r1) (* r1 (* r1 r0 83.0 83.0) r1 r1) 6618424257.0) 2.0 (* (/ r0 (/ 83.0 r2)) 2.0 r6 (* r1 r0 83.0 83.0))) (<= (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1))) (/ r8 6618424257.0)) v30) (and (= (* r1 r0 83.0 83.0) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)) r1) (>= 83.0 r2 (* r1 (* r1 r0 83.0 83.0) r1 r1) r1 83.0) v1 v10 v18 (> r1 (* r1 r0 83.0 83.0) r2 r3 r3)) v52) v26 (= (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)) (* (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)) r2 (* r1 (* r1 r0 83.0 83.0) r1 r1) (* r1 (* r1 r0 83.0 83.0) r1 r1) 6618424257.0) r2 (/ 83.0 (- r2)) (* (- (* 26664.0 (* r1 r0 83.0 83.0) (/ r0 (/ 83.0 r2)) r1 (* r1 (* r1 r0 83.0 83.0) r1 r1)) 26664.0 83.0) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1))))))
(assert (or v30 (>= (/ r2 (* (/ r0 (/ 83.0 r2)) 2.0 r6 (* r1 r0 83.0 83.0))) r4 (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (/ (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (* 26664.0 (* r1 r0 83.0 83.0) (/ r0 (/ 83.0 r2)) r1 (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (= (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)) (* (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)) r2 (* r1 (* r1 r0 83.0 83.0) r1 r1) (* r1 (* r1 r0 83.0 83.0) r1 r1) 6618424257.0) r2 (/ 83.0 (- r2)) (* (- (* 26664.0 (* r1 r0 83.0 83.0) (/ r0 (/ 83.0 r2)) r1 (* r1 (* r1 r0 83.0 83.0) r1 r1)) 26664.0 83.0) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1))))))
(assert (or v38 v38 v44))
(assert (or (and (and v12 v11 (>= 307769.0 r5) v40 (>= r6 (/ r0 (/ 83.0 r2)) (+ r1 r3 (* r1 r0 83.0 83.0) r2 r0) (* (- (* 26664.0 (* r1 r0 83.0 83.0) (/ r0 (/ 83.0 r2)) r1 (* r1 (* r1 r0 83.0 83.0) r1 r1)) 26664.0 83.0) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (<= (* (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)) r2 (* r1 (* r1 r0 83.0 83.0) r1 r1) (* r1 (* r1 r0 83.0 83.0) r1 r1) 6618424257.0) 2.0 (* (/ r0 (/ 83.0 r2)) 2.0 r6 (* r1 r0 83.0 83.0))) (<= (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1))) (/ r8 6618424257.0)) v30) (and (= (* r1 r0 83.0 83.0) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)) r1) (>= 83.0 r2 (* r1 (* r1 r0 83.0 83.0) r1 r1) r1 83.0) v1 v10 v18 (> r1 (* r1 r0 83.0 83.0) r2 r3 r3)) v52) (distinct (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1))))) (and (and v12 v11 (>= 307769.0 r5) v40 (>= r6 (/ r0 (/ 83.0 r2)) (+ r1 r3 (* r1 r0 83.0 83.0) r2 r0) (* (- (* 26664.0 (* r1 r0 83.0 83.0) (/ r0 (/ 83.0 r2)) r1 (* r1 (* r1 r0 83.0 83.0) r1 r1)) 26664.0 83.0) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (<= (* (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)) r2 (* r1 (* r1 r0 83.0 83.0) r1 r1) (* r1 (* r1 r0 83.0 83.0) r1 r1) 6618424257.0) 2.0 (* (/ r0 (/ 83.0 r2)) 2.0 r6 (* r1 r0 83.0 83.0))) (<= (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1))) (/ r8 6618424257.0)) v30) (and (= (* r1 r0 83.0 83.0) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)) r1) (>= 83.0 r2 (* r1 (* r1 r0 83.0 83.0) r1 r1) r1 83.0) v1 v10 v18 (> r1 (* r1 r0 83.0 83.0) r2 r3 r3)) v52)))
(assert (or v60 v26 (<= 26664.0 (- (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3)))))
(assert (or v44 v44 v60))
(assert (or v60 (<= (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (+ (- (* 26664.0 (* r1 r0 83.0 83.0) (/ r0 (/ 83.0 r2)) r1 (* r1 (* r1 r0 83.0 83.0) r1 r1)) 26664.0 83.0) (/ r8 6618424257.0) r2 26664.0) (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (/ r5 (/ (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (* 26664.0 (* r1 r0 83.0 83.0) (/ r0 (/ 83.0 r2)) r1 (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (* (- r2) (* r1 r0 83.0 83.0) r2 (/ 83.0 r2))) v30))
(assert (or v30 (and (and v12 v11 (>= 307769.0 r5) v40 (>= r6 (/ r0 (/ 83.0 r2)) (+ r1 r3 (* r1 r0 83.0 83.0) r2 r0) (* (- (* 26664.0 (* r1 r0 83.0 83.0) (/ r0 (/ 83.0 r2)) r1 (* r1 (* r1 r0 83.0 83.0) r1 r1)) 26664.0 83.0) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (<= (* (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)) r2 (* r1 (* r1 r0 83.0 83.0) r1 r1) (* r1 (* r1 r0 83.0 83.0) r1 r1) 6618424257.0) 2.0 (* (/ r0 (/ 83.0 r2)) 2.0 r6 (* r1 r0 83.0 83.0))) (<= (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1))) (/ r8 6618424257.0)) v30) (and (= (* r1 r0 83.0 83.0) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)) r1) (>= 83.0 r2 (* r1 (* r1 r0 83.0 83.0) r1 r1) r1 83.0) v1 v10 v18 (> r1 (* r1 r0 83.0 83.0) r2 r3 r3)) v52) (and (and v12 v11 (>= 307769.0 r5) v40 (>= r6 (/ r0 (/ 83.0 r2)) (+ r1 r3 (* r1 r0 83.0 83.0) r2 r0) (* (- (* 26664.0 (* r1 r0 83.0 83.0) (/ r0 (/ 83.0 r2)) r1 (* r1 (* r1 r0 83.0 83.0) r1 r1)) 26664.0 83.0) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (<= (* (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)) r2 (* r1 (* r1 r0 83.0 83.0) r1 r1) (* r1 (* r1 r0 83.0 83.0) r1 r1) 6618424257.0) 2.0 (* (/ r0 (/ 83.0 r2)) 2.0 r6 (* r1 r0 83.0 83.0))) (<= (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1))) (/ r8 6618424257.0)) v30) (and (= (* r1 r0 83.0 83.0) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)) r1) (>= 83.0 r2 (* r1 (* r1 r0 83.0 83.0) r1 r1) r1 83.0) v1 v10 v18 (> r1 (* r1 r0 83.0 83.0) r2 r3 r3)) v52)))
(assert (or (distinct (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1))))) v30 (< (- (* r1 r0 83.0 83.0)) (/ r8 6618424257.0))))
(assert (or v38 v39 (and (and v12 v11 (>= 307769.0 r5) v40 (>= r6 (/ r0 (/ 83.0 r2)) (+ r1 r3 (* r1 r0 83.0 83.0) r2 r0) (* (- (* 26664.0 (* r1 r0 83.0 83.0) (/ r0 (/ 83.0 r2)) r1 (* r1 (* r1 r0 83.0 83.0) r1 r1)) 26664.0 83.0) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (<= (* (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)) r2 (* r1 (* r1 r0 83.0 83.0) r1 r1) (* r1 (* r1 r0 83.0 83.0) r1 r1) 6618424257.0) 2.0 (* (/ r0 (/ 83.0 r2)) 2.0 r6 (* r1 r0 83.0 83.0))) (<= (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1))) (/ r8 6618424257.0)) v30) (and (= (* r1 r0 83.0 83.0) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)) r1) (>= 83.0 r2 (* r1 (* r1 r0 83.0 83.0) r1 r1) r1 83.0) v1 v10 v18 (> r1 (* r1 r0 83.0 83.0) r2 r3 r3)) v52)))
(assert (or v44 v44 (<= (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (+ (- (* 26664.0 (* r1 r0 83.0 83.0) (/ r0 (/ 83.0 r2)) r1 (* r1 (* r1 r0 83.0 83.0) r1 r1)) 26664.0 83.0) (/ r8 6618424257.0) r2 26664.0) (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (/ r5 (/ (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (* 26664.0 (* r1 r0 83.0 83.0) (/ r0 (/ 83.0 r2)) r1 (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (* (- r2) (* r1 r0 83.0 83.0) r2 (/ 83.0 r2)))))
(assert (or (>= (/ r2 (* (/ r0 (/ 83.0 r2)) 2.0 r6 (* r1 r0 83.0 83.0))) r4 (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (/ (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (* 26664.0 (* r1 r0 83.0 83.0) (/ r0 (/ 83.0 r2)) r1 (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (xor (>= (* r1 (* r1 r0 83.0 83.0) r1 r1) 2426.0 2426.0 6618424257.0) v59 v7) (<= 26664.0 (- (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3)))))
(assert (or v60 v26 (distinct (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))))))
(assert (or v38 (>= (/ r2 (* (/ r0 (/ 83.0 r2)) 2.0 r6 (* r1 r0 83.0 83.0))) r4 (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (/ (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (* 26664.0 (* r1 r0 83.0 83.0) (/ r0 (/ 83.0 r2)) r1 (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (distinct (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))))))
(assert (or v39 (>= (/ r2 (* (/ r0 (/ 83.0 r2)) 2.0 r6 (* r1 r0 83.0 83.0))) r4 (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (/ (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (* 26664.0 (* r1 r0 83.0 83.0) (/ r0 (/ 83.0 r2)) r1 (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (distinct (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))))))
(assert (or v44 (and (and v12 v11 (>= 307769.0 r5) v40 (>= r6 (/ r0 (/ 83.0 r2)) (+ r1 r3 (* r1 r0 83.0 83.0) r2 r0) (* (- (* 26664.0 (* r1 r0 83.0 83.0) (/ r0 (/ 83.0 r2)) r1 (* r1 (* r1 r0 83.0 83.0) r1 r1)) 26664.0 83.0) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (<= (* (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)) r2 (* r1 (* r1 r0 83.0 83.0) r1 r1) (* r1 (* r1 r0 83.0 83.0) r1 r1) 6618424257.0) 2.0 (* (/ r0 (/ 83.0 r2)) 2.0 r6 (* r1 r0 83.0 83.0))) (<= (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1))) (/ r8 6618424257.0)) v30) (and (= (* r1 r0 83.0 83.0) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)) r1) (>= 83.0 r2 (* r1 (* r1 r0 83.0 83.0) r1 r1) r1 83.0) v1 v10 v18 (> r1 (* r1 r0 83.0 83.0) r2 r3 r3)) v52) v44))
(assert (or (>= (/ r2 (* (/ r0 (/ 83.0 r2)) 2.0 r6 (* r1 r0 83.0 83.0))) r4 (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (/ (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (* 26664.0 (* r1 r0 83.0 83.0) (/ r0 (/ 83.0 r2)) r1 (* r1 (* r1 r0 83.0 83.0) r1 r1)))) v30 (and (and v12 v11 (>= 307769.0 r5) v40 (>= r6 (/ r0 (/ 83.0 r2)) (+ r1 r3 (* r1 r0 83.0 83.0) r2 r0) (* (- (* 26664.0 (* r1 r0 83.0 83.0) (/ r0 (/ 83.0 r2)) r1 (* r1 (* r1 r0 83.0 83.0) r1 r1)) 26664.0 83.0) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (<= (* (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)) r2 (* r1 (* r1 r0 83.0 83.0) r1 r1) (* r1 (* r1 r0 83.0 83.0) r1 r1) 6618424257.0) 2.0 (* (/ r0 (/ 83.0 r2)) 2.0 r6 (* r1 r0 83.0 83.0))) (<= (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1))) (/ r8 6618424257.0)) v30) (and (= (* r1 r0 83.0 83.0) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)) r1) (>= 83.0 r2 (* r1 (* r1 r0 83.0 83.0) r1 r1) r1 83.0) v1 v10 v18 (> r1 (* r1 r0 83.0 83.0) r2 r3 r3)) v52)))
(assert (or (<= 26664.0 (- (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3))) (= (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)) (* (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)) r2 (* r1 (* r1 r0 83.0 83.0) r1 r1) (* r1 (* r1 r0 83.0 83.0) r1 r1) 6618424257.0) r2 (/ 83.0 (- r2)) (* (- (* 26664.0 (* r1 r0 83.0 83.0) (/ r0 (/ 83.0 r2)) r1 (* r1 (* r1 r0 83.0 83.0) r1 r1)) 26664.0 83.0) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (<= 26664.0 (- (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3)))))
(assert (or (>= (/ r2 (* (/ r0 (/ 83.0 r2)) 2.0 r6 (* r1 r0 83.0 83.0))) r4 (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (/ (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (* 26664.0 (* r1 r0 83.0 83.0) (/ r0 (/ 83.0 r2)) r1 (* r1 (* r1 r0 83.0 83.0) r1 r1)))) v60 v60))
(assert (or (< (- (* r1 r0 83.0 83.0)) (/ r8 6618424257.0)) (<= (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (+ (- (* 26664.0 (* r1 r0 83.0 83.0) (/ r0 (/ 83.0 r2)) r1 (* r1 (* r1 r0 83.0 83.0) r1 r1)) 26664.0 83.0) (/ r8 6618424257.0) r2 26664.0) (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (/ r5 (/ (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (* 26664.0 (* r1 r0 83.0 83.0) (/ r0 (/ 83.0 r2)) r1 (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (* (- r2) (* r1 r0 83.0 83.0) r2 (/ 83.0 r2))) v5))
(assert (or (xor (>= (* r1 (* r1 r0 83.0 83.0) r1 r1) 2426.0 2426.0 6618424257.0) v59 v7) v26 v60))
(assert (or v30 v60 v39))
(assert (or (<= (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (+ (- (* 26664.0 (* r1 r0 83.0 83.0) (/ r0 (/ 83.0 r2)) r1 (* r1 (* r1 r0 83.0 83.0) r1 r1)) 26664.0 83.0) (/ r8 6618424257.0) r2 26664.0) (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (/ r5 (/ (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (* 26664.0 (* r1 r0 83.0 83.0) (/ r0 (/ 83.0 r2)) r1 (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (* (- r2) (* r1 r0 83.0 83.0) r2 (/ 83.0 r2))) (<= 26664.0 (- r1)) (< (- (* r1 r0 83.0 83.0)) (/ r8 6618424257.0))))
(assert (or (< (- (* r1 r0 83.0 83.0)) (/ r8 6618424257.0)) v44 v39))
(assert (or (distinct (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1))))) (>= (/ r2 (* (/ r0 (/ 83.0 r2)) 2.0 r6 (* r1 r0 83.0 83.0))) r4 (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (/ (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (* 26664.0 (* r1 r0 83.0 83.0) (/ r0 (/ 83.0 r2)) r1 (* r1 (* r1 r0 83.0 83.0) r1 r1)))) v60))
(assert (or (< (- (* r1 r0 83.0 83.0)) (/ r8 6618424257.0)) v60 v26))
(assert (or (<= (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (+ (- (* 26664.0 (* r1 r0 83.0 83.0) (/ r0 (/ 83.0 r2)) r1 (* r1 (* r1 r0 83.0 83.0) r1 r1)) 26664.0 83.0) (/ r8 6618424257.0) r2 26664.0) (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (/ r5 (/ (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (* 26664.0 (* r1 r0 83.0 83.0) (/ r0 (/ 83.0 r2)) r1 (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (* (- r2) (* r1 r0 83.0 83.0) r2 (/ 83.0 r2))) (= (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)) (* (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)) r2 (* r1 (* r1 r0 83.0 83.0) r1 r1) (* r1 (* r1 r0 83.0 83.0) r1 r1) 6618424257.0) r2 (/ 83.0 (- r2)) (* (- (* 26664.0 (* r1 r0 83.0 83.0) (/ r0 (/ 83.0 r2)) r1 (* r1 (* r1 r0 83.0 83.0) r1 r1)) 26664.0 83.0) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (<= (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (+ (- (* 26664.0 (* r1 r0 83.0 83.0) (/ r0 (/ 83.0 r2)) r1 (* r1 (* r1 r0 83.0 83.0) r1 r1)) 26664.0 83.0) (/ r8 6618424257.0) r2 26664.0) (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (/ r5 (/ (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (* 26664.0 (* r1 r0 83.0 83.0) (/ r0 (/ 83.0 r2)) r1 (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (* (- r2) (* r1 r0 83.0 83.0) r2 (/ 83.0 r2)))))
(assert (or (distinct (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1))))) (<= 26664.0 (- (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3))) v26))
(assert (or (distinct (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1))))) (= (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)) (* (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)) r2 (* r1 (* r1 r0 83.0 83.0) r1 r1) (* r1 (* r1 r0 83.0 83.0) r1 r1) 6618424257.0) r2 (/ 83.0 (- r2)) (* (- (* 26664.0 (* r1 r0 83.0 83.0) (/ r0 (/ 83.0 r2)) r1 (* r1 (* r1 r0 83.0 83.0) r1 r1)) 26664.0 83.0) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) v39))
(assert (or v26 (>= (/ r2 (* (/ r0 (/ 83.0 r2)) 2.0 r6 (* r1 r0 83.0 83.0))) r4 (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (/ (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (* 26664.0 (* r1 r0 83.0 83.0) (/ r0 (/ 83.0 r2)) r1 (* r1 (* r1 r0 83.0 83.0) r1 r1)))) v44))
(assert (or (distinct (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1))))) (distinct (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1))))) (= (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)) (* (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)) r2 (* r1 (* r1 r0 83.0 83.0) r1 r1) (* r1 (* r1 r0 83.0 83.0) r1 r1) 6618424257.0) r2 (/ 83.0 (- r2)) (* (- (* 26664.0 (* r1 r0 83.0 83.0) (/ r0 (/ 83.0 r2)) r1 (* r1 (* r1 r0 83.0 83.0) r1 r1)) 26664.0 83.0) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1))))))
(assert (or (xor (>= (* r1 (* r1 r0 83.0 83.0) r1 r1) 2426.0 2426.0 6618424257.0) v59 v7) (<= 26664.0 (- (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3))) v39))
(assert (or (< (- (* r1 r0 83.0 83.0)) (/ r8 6618424257.0)) (<= 26664.0 (- (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3))) v39))
(assert (or v26 (and (and v12 v11 (>= 307769.0 r5) v40 (>= r6 (/ r0 (/ 83.0 r2)) (+ r1 r3 (* r1 r0 83.0 83.0) r2 r0) (* (- (* 26664.0 (* r1 r0 83.0 83.0) (/ r0 (/ 83.0 r2)) r1 (* r1 (* r1 r0 83.0 83.0) r1 r1)) 26664.0 83.0) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (<= (* (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)) r2 (* r1 (* r1 r0 83.0 83.0) r1 r1) (* r1 (* r1 r0 83.0 83.0) r1 r1) 6618424257.0) 2.0 (* (/ r0 (/ 83.0 r2)) 2.0 r6 (* r1 r0 83.0 83.0))) (<= (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1))) (/ r8 6618424257.0)) v30) (and (= (* r1 r0 83.0 83.0) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)) r1) (>= 83.0 r2 (* r1 (* r1 r0 83.0 83.0) r1 r1) r1 83.0) v1 v10 v18 (> r1 (* r1 r0 83.0 83.0) r2 r3 r3)) v52) v44))
(assert (or (<= 26664.0 (- r1)) (>= (/ r2 (* (/ r0 (/ 83.0 r2)) 2.0 r6 (* r1 r0 83.0 83.0))) r4 (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (/ (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (* 26664.0 (* r1 r0 83.0 83.0) (/ r0 (/ 83.0 r2)) r1 (* r1 (* r1 r0 83.0 83.0) r1 r1)))) v26))
(assert (or (>= (/ r2 (* (/ r0 (/ 83.0 r2)) 2.0 r6 (* r1 r0 83.0 83.0))) r4 (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (/ (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (* 26664.0 (* r1 r0 83.0 83.0) (/ r0 (/ 83.0 r2)) r1 (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (distinct (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1))))) v30))
(assert (or v26 (and (and v12 v11 (>= 307769.0 r5) v40 (>= r6 (/ r0 (/ 83.0 r2)) (+ r1 r3 (* r1 r0 83.0 83.0) r2 r0) (* (- (* 26664.0 (* r1 r0 83.0 83.0) (/ r0 (/ 83.0 r2)) r1 (* r1 (* r1 r0 83.0 83.0) r1 r1)) 26664.0 83.0) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (<= (* (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)) r2 (* r1 (* r1 r0 83.0 83.0) r1 r1) (* r1 (* r1 r0 83.0 83.0) r1 r1) 6618424257.0) 2.0 (* (/ r0 (/ 83.0 r2)) 2.0 r6 (* r1 r0 83.0 83.0))) (<= (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1))) (/ r8 6618424257.0)) v30) (and (= (* r1 r0 83.0 83.0) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)) r1) (>= 83.0 r2 (* r1 (* r1 r0 83.0 83.0) r1 r1) r1 83.0) v1 v10 v18 (> r1 (* r1 r0 83.0 83.0) r2 r3 r3)) v52) (>= (/ r2 (* (/ r0 (/ 83.0 r2)) 2.0 r6 (* r1 r0 83.0 83.0))) r4 (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (/ (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (* 26664.0 (* r1 r0 83.0 83.0) (/ r0 (/ 83.0 r2)) r1 (* r1 (* r1 r0 83.0 83.0) r1 r1))))))
(assert (or (<= (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (+ (- (* 26664.0 (* r1 r0 83.0 83.0) (/ r0 (/ 83.0 r2)) r1 (* r1 (* r1 r0 83.0 83.0) r1 r1)) 26664.0 83.0) (/ r8 6618424257.0) r2 26664.0) (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (/ r5 (/ (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (* 26664.0 (* r1 r0 83.0 83.0) (/ r0 (/ 83.0 r2)) r1 (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (* (- r2) (* r1 r0 83.0 83.0) r2 (/ 83.0 r2))) v38 v26))
(assert (or (< (- (* r1 r0 83.0 83.0)) (/ r8 6618424257.0)) v30 v26))
(assert (or (<= 26664.0 (- (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3))) (<= 26664.0 (- r1)) (<= (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (+ (- (* 26664.0 (* r1 r0 83.0 83.0) (/ r0 (/ 83.0 r2)) r1 (* r1 (* r1 r0 83.0 83.0) r1 r1)) 26664.0 83.0) (/ r8 6618424257.0) r2 26664.0) (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (/ r5 (/ (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (* 26664.0 (* r1 r0 83.0 83.0) (/ r0 (/ 83.0 r2)) r1 (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (* (- r2) (* r1 r0 83.0 83.0) r2 (/ 83.0 r2)))))
(assert (or (<= (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (+ (- (* 26664.0 (* r1 r0 83.0 83.0) (/ r0 (/ 83.0 r2)) r1 (* r1 (* r1 r0 83.0 83.0) r1 r1)) 26664.0 83.0) (/ r8 6618424257.0) r2 26664.0) (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (/ r5 (/ (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (* 26664.0 (* r1 r0 83.0 83.0) (/ r0 (/ 83.0 r2)) r1 (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (* (- r2) (* r1 r0 83.0 83.0) r2 (/ 83.0 r2))) (distinct (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1))))) (< (- (* r1 r0 83.0 83.0)) (/ r8 6618424257.0))))
(assert (or v26 (<= 26664.0 (- r1)) v5))
(assert (or (distinct (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1))))) v44 (< (- (* r1 r0 83.0 83.0)) (/ r8 6618424257.0))))
(assert (or (= (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)) (* (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)) r2 (* r1 (* r1 r0 83.0 83.0) r1 r1) (* r1 (* r1 r0 83.0 83.0) r1 r1) 6618424257.0) r2 (/ 83.0 (- r2)) (* (- (* 26664.0 (* r1 r0 83.0 83.0) (/ r0 (/ 83.0 r2)) r1 (* r1 (* r1 r0 83.0 83.0) r1 r1)) 26664.0 83.0) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (<= 26664.0 (- r1)) (< (- (* r1 r0 83.0 83.0)) (/ r8 6618424257.0))))
(assert (or v60 v60 (= (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)) (* (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)) r2 (* r1 (* r1 r0 83.0 83.0) r1 r1) (* r1 (* r1 r0 83.0 83.0) r1 r1) 6618424257.0) r2 (/ 83.0 (- r2)) (* (- (* 26664.0 (* r1 r0 83.0 83.0) (/ r0 (/ 83.0 r2)) r1 (* r1 (* r1 r0 83.0 83.0) r1 r1)) 26664.0 83.0) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1))))))
(assert (or v26 (= (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)) (* (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)) r2 (* r1 (* r1 r0 83.0 83.0) r1 r1) (* r1 (* r1 r0 83.0 83.0) r1 r1) 6618424257.0) r2 (/ 83.0 (- r2)) (* (- (* 26664.0 (* r1 r0 83.0 83.0) (/ r0 (/ 83.0 r2)) r1 (* r1 (* r1 r0 83.0 83.0) r1 r1)) 26664.0 83.0) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (distinct (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))))))
(assert (or v38 v26 (< (- (* r1 r0 83.0 83.0)) (/ r8 6618424257.0))))
(assert (or v39 v38 (xor (>= (* r1 (* r1 r0 83.0 83.0) r1 r1) 2426.0 2426.0 6618424257.0) v59 v7)))
(assert (or (distinct (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1))))) v38 (<= 26664.0 (- (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3)))))
(assert (or v38 (< (- (* r1 r0 83.0 83.0)) (/ r8 6618424257.0)) (>= (/ r2 (* (/ r0 (/ 83.0 r2)) 2.0 r6 (* r1 r0 83.0 83.0))) r4 (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (/ (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (* 26664.0 (* r1 r0 83.0 83.0) (/ r0 (/ 83.0 r2)) r1 (* r1 (* r1 r0 83.0 83.0) r1 r1))))))
(assert (or v39 v39 (and (and v12 v11 (>= 307769.0 r5) v40 (>= r6 (/ r0 (/ 83.0 r2)) (+ r1 r3 (* r1 r0 83.0 83.0) r2 r0) (* (- (* 26664.0 (* r1 r0 83.0 83.0) (/ r0 (/ 83.0 r2)) r1 (* r1 (* r1 r0 83.0 83.0) r1 r1)) 26664.0 83.0) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (<= (* (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)) r2 (* r1 (* r1 r0 83.0 83.0) r1 r1) (* r1 (* r1 r0 83.0 83.0) r1 r1) 6618424257.0) 2.0 (* (/ r0 (/ 83.0 r2)) 2.0 r6 (* r1 r0 83.0 83.0))) (<= (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1))) (/ r8 6618424257.0)) v30) (and (= (* r1 r0 83.0 83.0) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)) r1) (>= 83.0 r2 (* r1 (* r1 r0 83.0 83.0) r1 r1) r1 83.0) v1 v10 v18 (> r1 (* r1 r0 83.0 83.0) r2 r3 r3)) v52)))
(assert (or v26 (<= 26664.0 (- (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3))) v38))
(assert (or (<= 26664.0 (- r1)) v5 (xor (>= (* r1 (* r1 r0 83.0 83.0) r1 r1) 2426.0 2426.0 6618424257.0) v59 v7)))
(assert (or (<= 26664.0 (- (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3))) (>= (/ r2 (* (/ r0 (/ 83.0 r2)) 2.0 r6 (* r1 r0 83.0 83.0))) r4 (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (/ (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (* 26664.0 (* r1 r0 83.0 83.0) (/ r0 (/ 83.0 r2)) r1 (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (<= 26664.0 (- (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3)))))
(assert (or v30 v39 (<= 26664.0 (- r1))))
(assert (or v39 (<= 26664.0 (- (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3))) v30))
(assert (or (distinct (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1))))) (<= (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (+ (- (* 26664.0 (* r1 r0 83.0 83.0) (/ r0 (/ 83.0 r2)) r1 (* r1 (* r1 r0 83.0 83.0) r1 r1)) 26664.0 83.0) (/ r8 6618424257.0) r2 26664.0) (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (/ r5 (/ (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (* 26664.0 (* r1 r0 83.0 83.0) (/ r0 (/ 83.0 r2)) r1 (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (* (- r2) (* r1 r0 83.0 83.0) r2 (/ 83.0 r2))) (xor (>= (* r1 (* r1 r0 83.0 83.0) r1 r1) 2426.0 2426.0 6618424257.0) v59 v7)))
(assert (or (and (and v12 v11 (>= 307769.0 r5) v40 (>= r6 (/ r0 (/ 83.0 r2)) (+ r1 r3 (* r1 r0 83.0 83.0) r2 r0) (* (- (* 26664.0 (* r1 r0 83.0 83.0) (/ r0 (/ 83.0 r2)) r1 (* r1 (* r1 r0 83.0 83.0) r1 r1)) 26664.0 83.0) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (<= (* (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)) r2 (* r1 (* r1 r0 83.0 83.0) r1 r1) (* r1 (* r1 r0 83.0 83.0) r1 r1) 6618424257.0) 2.0 (* (/ r0 (/ 83.0 r2)) 2.0 r6 (* r1 r0 83.0 83.0))) (<= (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1))) (/ r8 6618424257.0)) v30) (and (= (* r1 r0 83.0 83.0) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)) r1) (>= 83.0 r2 (* r1 (* r1 r0 83.0 83.0) r1 r1) r1 83.0) v1 v10 v18 (> r1 (* r1 r0 83.0 83.0) r2 r3 r3)) v52) v44 (<= 26664.0 (- r1))))
(assert (or (<= 26664.0 (- r1)) (distinct (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1))))) (xor (>= (* r1 (* r1 r0 83.0 83.0) r1 r1) 2426.0 2426.0 6618424257.0) v59 v7)))
(assert (or v30 v5 v39))
(assert (or (xor (>= (* r1 (* r1 r0 83.0 83.0) r1 r1) 2426.0 2426.0 6618424257.0) v59 v7) (<= 26664.0 (- (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3))) (and (and v12 v11 (>= 307769.0 r5) v40 (>= r6 (/ r0 (/ 83.0 r2)) (+ r1 r3 (* r1 r0 83.0 83.0) r2 r0) (* (- (* 26664.0 (* r1 r0 83.0 83.0) (/ r0 (/ 83.0 r2)) r1 (* r1 (* r1 r0 83.0 83.0) r1 r1)) 26664.0 83.0) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (<= (* (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)) r2 (* r1 (* r1 r0 83.0 83.0) r1 r1) (* r1 (* r1 r0 83.0 83.0) r1 r1) 6618424257.0) 2.0 (* (/ r0 (/ 83.0 r2)) 2.0 r6 (* r1 r0 83.0 83.0))) (<= (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1))) (/ r8 6618424257.0)) v30) (and (= (* r1 r0 83.0 83.0) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)) r1) (>= 83.0 r2 (* r1 (* r1 r0 83.0 83.0) r1 r1) r1 83.0) v1 v10 v18 (> r1 (* r1 r0 83.0 83.0) r2 r3 r3)) v52)))
(assert (or v44 v26 v26))
(assert (or v30 v38 (<= 26664.0 (- (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3)))))
(assert (or v38 v38 (distinct (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))))))
(assert (or (= (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)) (* (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)) r2 (* r1 (* r1 r0 83.0 83.0) r1 r1) (* r1 (* r1 r0 83.0 83.0) r1 r1) 6618424257.0) r2 (/ 83.0 (- r2)) (* (- (* 26664.0 (* r1 r0 83.0 83.0) (/ r0 (/ 83.0 r2)) r1 (* r1 (* r1 r0 83.0 83.0) r1 r1)) 26664.0 83.0) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (and (and v12 v11 (>= 307769.0 r5) v40 (>= r6 (/ r0 (/ 83.0 r2)) (+ r1 r3 (* r1 r0 83.0 83.0) r2 r0) (* (- (* 26664.0 (* r1 r0 83.0 83.0) (/ r0 (/ 83.0 r2)) r1 (* r1 (* r1 r0 83.0 83.0) r1 r1)) 26664.0 83.0) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (<= (* (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)) r2 (* r1 (* r1 r0 83.0 83.0) r1 r1) (* r1 (* r1 r0 83.0 83.0) r1 r1) 6618424257.0) 2.0 (* (/ r0 (/ 83.0 r2)) 2.0 r6 (* r1 r0 83.0 83.0))) (<= (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1))) (/ r8 6618424257.0)) v30) (and (= (* r1 r0 83.0 83.0) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)) r1) (>= 83.0 r2 (* r1 (* r1 r0 83.0 83.0) r1 r1) r1 83.0) v1 v10 v18 (> r1 (* r1 r0 83.0 83.0) r2 r3 r3)) v52) v26))
(assert (or (and (and v12 v11 (>= 307769.0 r5) v40 (>= r6 (/ r0 (/ 83.0 r2)) (+ r1 r3 (* r1 r0 83.0 83.0) r2 r0) (* (- (* 26664.0 (* r1 r0 83.0 83.0) (/ r0 (/ 83.0 r2)) r1 (* r1 (* r1 r0 83.0 83.0) r1 r1)) 26664.0 83.0) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (<= (* (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)) r2 (* r1 (* r1 r0 83.0 83.0) r1 r1) (* r1 (* r1 r0 83.0 83.0) r1 r1) 6618424257.0) 2.0 (* (/ r0 (/ 83.0 r2)) 2.0 r6 (* r1 r0 83.0 83.0))) (<= (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1))) (/ r8 6618424257.0)) v30) (and (= (* r1 r0 83.0 83.0) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)) r1) (>= 83.0 r2 (* r1 (* r1 r0 83.0 83.0) r1 r1) r1 83.0) v1 v10 v18 (> r1 (* r1 r0 83.0 83.0) r2 r3 r3)) v52) (>= (/ r2 (* (/ r0 (/ 83.0 r2)) 2.0 r6 (* r1 r0 83.0 83.0))) r4 (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (/ (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (* 26664.0 (* r1 r0 83.0 83.0) (/ r0 (/ 83.0 r2)) r1 (* r1 (* r1 r0 83.0 83.0) r1 r1)))) v5))
(assert (or (= (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)) (* (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)) r2 (* r1 (* r1 r0 83.0 83.0) r1 r1) (* r1 (* r1 r0 83.0 83.0) r1 r1) 6618424257.0) r2 (/ 83.0 (- r2)) (* (- (* 26664.0 (* r1 r0 83.0 83.0) (/ r0 (/ 83.0 r2)) r1 (* r1 (* r1 r0 83.0 83.0) r1 r1)) 26664.0 83.0) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) v38 (<= 26664.0 (- (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3)))))
(assert (or v30 (xor (>= (* r1 (* r1 r0 83.0 83.0) r1 r1) 2426.0 2426.0 6618424257.0) v59 v7) (<= 26664.0 (- (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3)))))
(assert (or (xor (>= (* r1 (* r1 r0 83.0 83.0) r1 r1) 2426.0 2426.0 6618424257.0) v59 v7) (<= 26664.0 (- r1)) v44))
(assert (or v38 (< (- (* r1 r0 83.0 83.0)) (/ r8 6618424257.0)) v5))
(assert (or (<= 26664.0 (- r1)) v5 (<= 26664.0 (- (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3)))))
(assert (or (= (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)) (* (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)) r2 (* r1 (* r1 r0 83.0 83.0) r1 r1) (* r1 (* r1 r0 83.0 83.0) r1 r1) 6618424257.0) r2 (/ 83.0 (- r2)) (* (- (* 26664.0 (* r1 r0 83.0 83.0) (/ r0 (/ 83.0 r2)) r1 (* r1 (* r1 r0 83.0 83.0) r1 r1)) 26664.0 83.0) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (and (and v12 v11 (>= 307769.0 r5) v40 (>= r6 (/ r0 (/ 83.0 r2)) (+ r1 r3 (* r1 r0 83.0 83.0) r2 r0) (* (- (* 26664.0 (* r1 r0 83.0 83.0) (/ r0 (/ 83.0 r2)) r1 (* r1 (* r1 r0 83.0 83.0) r1 r1)) 26664.0 83.0) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (<= (* (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)) r2 (* r1 (* r1 r0 83.0 83.0) r1 r1) (* r1 (* r1 r0 83.0 83.0) r1 r1) 6618424257.0) 2.0 (* (/ r0 (/ 83.0 r2)) 2.0 r6 (* r1 r0 83.0 83.0))) (<= (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1))) (/ r8 6618424257.0)) v30) (and (= (* r1 r0 83.0 83.0) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)) r1) (>= 83.0 r2 (* r1 (* r1 r0 83.0 83.0) r1 r1) r1 83.0) v1 v10 v18 (> r1 (* r1 r0 83.0 83.0) r2 r3 r3)) v52) (<= (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (+ (- (* 26664.0 (* r1 r0 83.0 83.0) (/ r0 (/ 83.0 r2)) r1 (* r1 (* r1 r0 83.0 83.0) r1 r1)) 26664.0 83.0) (/ r8 6618424257.0) r2 26664.0) (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (/ r5 (/ (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (* 26664.0 (* r1 r0 83.0 83.0) (/ r0 (/ 83.0 r2)) r1 (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (* (- r2) (* r1 r0 83.0 83.0) r2 (/ 83.0 r2)))))
(assert (or (<= 26664.0 (- (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3))) (= (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)) (* (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)) r2 (* r1 (* r1 r0 83.0 83.0) r1 r1) (* r1 (* r1 r0 83.0 83.0) r1 r1) 6618424257.0) r2 (/ 83.0 (- r2)) (* (- (* 26664.0 (* r1 r0 83.0 83.0) (/ r0 (/ 83.0 r2)) r1 (* r1 (* r1 r0 83.0 83.0) r1 r1)) 26664.0 83.0) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (and (and v12 v11 (>= 307769.0 r5) v40 (>= r6 (/ r0 (/ 83.0 r2)) (+ r1 r3 (* r1 r0 83.0 83.0) r2 r0) (* (- (* 26664.0 (* r1 r0 83.0 83.0) (/ r0 (/ 83.0 r2)) r1 (* r1 (* r1 r0 83.0 83.0) r1 r1)) 26664.0 83.0) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (<= (* (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)) r2 (* r1 (* r1 r0 83.0 83.0) r1 r1) (* r1 (* r1 r0 83.0 83.0) r1 r1) 6618424257.0) 2.0 (* (/ r0 (/ 83.0 r2)) 2.0 r6 (* r1 r0 83.0 83.0))) (<= (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1))) (/ r8 6618424257.0)) v30) (and (= (* r1 r0 83.0 83.0) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)) r1) (>= 83.0 r2 (* r1 (* r1 r0 83.0 83.0) r1 r1) r1 83.0) v1 v10 v18 (> r1 (* r1 r0 83.0 83.0) r2 r3 r3)) v52)))
(assert (or (<= (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (+ (- (* 26664.0 (* r1 r0 83.0 83.0) (/ r0 (/ 83.0 r2)) r1 (* r1 (* r1 r0 83.0 83.0) r1 r1)) 26664.0 83.0) (/ r8 6618424257.0) r2 26664.0) (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (/ r5 (/ (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (* 26664.0 (* r1 r0 83.0 83.0) (/ r0 (/ 83.0 r2)) r1 (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (* (- r2) (* r1 r0 83.0 83.0) r2 (/ 83.0 r2))) v39 v30))
(assert (or (and (and v12 v11 (>= 307769.0 r5) v40 (>= r6 (/ r0 (/ 83.0 r2)) (+ r1 r3 (* r1 r0 83.0 83.0) r2 r0) (* (- (* 26664.0 (* r1 r0 83.0 83.0) (/ r0 (/ 83.0 r2)) r1 (* r1 (* r1 r0 83.0 83.0) r1 r1)) 26664.0 83.0) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (<= (* (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)) r2 (* r1 (* r1 r0 83.0 83.0) r1 r1) (* r1 (* r1 r0 83.0 83.0) r1 r1) 6618424257.0) 2.0 (* (/ r0 (/ 83.0 r2)) 2.0 r6 (* r1 r0 83.0 83.0))) (<= (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1))) (/ r8 6618424257.0)) v30) (and (= (* r1 r0 83.0 83.0) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)) r1) (>= 83.0 r2 (* r1 (* r1 r0 83.0 83.0) r1 r1) r1 83.0) v1 v10 v18 (> r1 (* r1 r0 83.0 83.0) r2 r3 r3)) v52) (<= (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (+ (- (* 26664.0 (* r1 r0 83.0 83.0) (/ r0 (/ 83.0 r2)) r1 (* r1 (* r1 r0 83.0 83.0) r1 r1)) 26664.0 83.0) (/ r8 6618424257.0) r2 26664.0) (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (/ r5 (/ (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (* 26664.0 (* r1 r0 83.0 83.0) (/ r0 (/ 83.0 r2)) r1 (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (* (- r2) (* r1 r0 83.0 83.0) r2 (/ 83.0 r2))) (and (and v12 v11 (>= 307769.0 r5) v40 (>= r6 (/ r0 (/ 83.0 r2)) (+ r1 r3 (* r1 r0 83.0 83.0) r2 r0) (* (- (* 26664.0 (* r1 r0 83.0 83.0) (/ r0 (/ 83.0 r2)) r1 (* r1 (* r1 r0 83.0 83.0) r1 r1)) 26664.0 83.0) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (<= (* (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)) r2 (* r1 (* r1 r0 83.0 83.0) r1 r1) (* r1 (* r1 r0 83.0 83.0) r1 r1) 6618424257.0) 2.0 (* (/ r0 (/ 83.0 r2)) 2.0 r6 (* r1 r0 83.0 83.0))) (<= (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1))) (/ r8 6618424257.0)) v30) (and (= (* r1 r0 83.0 83.0) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)) r1) (>= 83.0 r2 (* r1 (* r1 r0 83.0 83.0) r1 r1) r1 83.0) v1 v10 v18 (> r1 (* r1 r0 83.0 83.0) r2 r3 r3)) v52)))
(assert (or v5 (xor (>= (* r1 (* r1 r0 83.0 83.0) r1 r1) 2426.0 2426.0 6618424257.0) v59 v7) v26))
(assert (or (<= 26664.0 (- r1)) (<= (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (+ (- (* 26664.0 (* r1 r0 83.0 83.0) (/ r0 (/ 83.0 r2)) r1 (* r1 (* r1 r0 83.0 83.0) r1 r1)) 26664.0 83.0) (/ r8 6618424257.0) r2 26664.0) (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (/ r5 (/ (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (* 26664.0 (* r1 r0 83.0 83.0) (/ r0 (/ 83.0 r2)) r1 (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (* (- r2) (* r1 r0 83.0 83.0) r2 (/ 83.0 r2))) v60))
(assert (or v44 (<= (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (+ (- (* 26664.0 (* r1 r0 83.0 83.0) (/ r0 (/ 83.0 r2)) r1 (* r1 (* r1 r0 83.0 83.0) r1 r1)) 26664.0 83.0) (/ r8 6618424257.0) r2 26664.0) (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (/ r5 (/ (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (* 26664.0 (* r1 r0 83.0 83.0) (/ r0 (/ 83.0 r2)) r1 (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (* (- r2) (* r1 r0 83.0 83.0) r2 (/ 83.0 r2))) (< (- (* r1 r0 83.0 83.0)) (/ r8 6618424257.0))))
(assert (or (= (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)) (* (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)) r2 (* r1 (* r1 r0 83.0 83.0) r1 r1) (* r1 (* r1 r0 83.0 83.0) r1 r1) 6618424257.0) r2 (/ 83.0 (- r2)) (* (- (* 26664.0 (* r1 r0 83.0 83.0) (/ r0 (/ 83.0 r2)) r1 (* r1 (* r1 r0 83.0 83.0) r1 r1)) 26664.0 83.0) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) v26 v39))
(assert (or (< (- (* r1 r0 83.0 83.0)) (/ r8 6618424257.0)) (<= 26664.0 (- (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3))) (<= 26664.0 (- (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3)))))
(assert (or (distinct (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1))))) (< (- (* r1 r0 83.0 83.0)) (/ r8 6618424257.0)) v5))
(assert (or v39 v26 (<= (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (+ (- (* 26664.0 (* r1 r0 83.0 83.0) (/ r0 (/ 83.0 r2)) r1 (* r1 (* r1 r0 83.0 83.0) r1 r1)) 26664.0 83.0) (/ r8 6618424257.0) r2 26664.0) (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (/ r5 (/ (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (* 26664.0 (* r1 r0 83.0 83.0) (/ r0 (/ 83.0 r2)) r1 (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (* (- r2) (* r1 r0 83.0 83.0) r2 (/ 83.0 r2)))))
(assert (or (< (- (* r1 r0 83.0 83.0)) (/ r8 6618424257.0)) (and (and v12 v11 (>= 307769.0 r5) v40 (>= r6 (/ r0 (/ 83.0 r2)) (+ r1 r3 (* r1 r0 83.0 83.0) r2 r0) (* (- (* 26664.0 (* r1 r0 83.0 83.0) (/ r0 (/ 83.0 r2)) r1 (* r1 (* r1 r0 83.0 83.0) r1 r1)) 26664.0 83.0) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (<= (* (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)) r2 (* r1 (* r1 r0 83.0 83.0) r1 r1) (* r1 (* r1 r0 83.0 83.0) r1 r1) 6618424257.0) 2.0 (* (/ r0 (/ 83.0 r2)) 2.0 r6 (* r1 r0 83.0 83.0))) (<= (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1))) (/ r8 6618424257.0)) v30) (and (= (* r1 r0 83.0 83.0) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)) r1) (>= 83.0 r2 (* r1 (* r1 r0 83.0 83.0) r1 r1) r1 83.0) v1 v10 v18 (> r1 (* r1 r0 83.0 83.0) r2 r3 r3)) v52) (xor (>= (* r1 (* r1 r0 83.0 83.0) r1 r1) 2426.0 2426.0 6618424257.0) v59 v7)))
(assert (or (xor (>= (* r1 (* r1 r0 83.0 83.0) r1 r1) 2426.0 2426.0 6618424257.0) v59 v7) v26 (= (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)) (* (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)) r2 (* r1 (* r1 r0 83.0 83.0) r1 r1) (* r1 (* r1 r0 83.0 83.0) r1 r1) 6618424257.0) r2 (/ 83.0 (- r2)) (* (- (* 26664.0 (* r1 r0 83.0 83.0) (/ r0 (/ 83.0 r2)) r1 (* r1 (* r1 r0 83.0 83.0) r1 r1)) 26664.0 83.0) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1))))))
(assert (or (and (and v12 v11 (>= 307769.0 r5) v40 (>= r6 (/ r0 (/ 83.0 r2)) (+ r1 r3 (* r1 r0 83.0 83.0) r2 r0) (* (- (* 26664.0 (* r1 r0 83.0 83.0) (/ r0 (/ 83.0 r2)) r1 (* r1 (* r1 r0 83.0 83.0) r1 r1)) 26664.0 83.0) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (<= (* (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)) r2 (* r1 (* r1 r0 83.0 83.0) r1 r1) (* r1 (* r1 r0 83.0 83.0) r1 r1) 6618424257.0) 2.0 (* (/ r0 (/ 83.0 r2)) 2.0 r6 (* r1 r0 83.0 83.0))) (<= (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1))) (/ r8 6618424257.0)) v30) (and (= (* r1 r0 83.0 83.0) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)) r1) (>= 83.0 r2 (* r1 (* r1 r0 83.0 83.0) r1 r1) r1 83.0) v1 v10 v18 (> r1 (* r1 r0 83.0 83.0) r2 r3 r3)) v52) v5 v38))
(assert (or (<= 26664.0 (- r1)) v26 (<= (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (+ (- (* 26664.0 (* r1 r0 83.0 83.0) (/ r0 (/ 83.0 r2)) r1 (* r1 (* r1 r0 83.0 83.0) r1 r1)) 26664.0 83.0) (/ r8 6618424257.0) r2 26664.0) (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (/ r5 (/ (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (* 26664.0 (* r1 r0 83.0 83.0) (/ r0 (/ 83.0 r2)) r1 (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (* (- r2) (* r1 r0 83.0 83.0) r2 (/ 83.0 r2)))))
(assert (or (<= 26664.0 (- r1)) (<= (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (+ (- (* 26664.0 (* r1 r0 83.0 83.0) (/ r0 (/ 83.0 r2)) r1 (* r1 (* r1 r0 83.0 83.0) r1 r1)) 26664.0 83.0) (/ r8 6618424257.0) r2 26664.0) (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (/ r5 (/ (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (* 26664.0 (* r1 r0 83.0 83.0) (/ r0 (/ 83.0 r2)) r1 (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (* (- r2) (* r1 r0 83.0 83.0) r2 (/ 83.0 r2))) (= (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)) (* (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)) r2 (* r1 (* r1 r0 83.0 83.0) r1 r1) (* r1 (* r1 r0 83.0 83.0) r1 r1) 6618424257.0) r2 (/ 83.0 (- r2)) (* (- (* 26664.0 (* r1 r0 83.0 83.0) (/ r0 (/ 83.0 r2)) r1 (* r1 (* r1 r0 83.0 83.0) r1 r1)) 26664.0 83.0) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1))))))
(assert (or v5 (xor (>= (* r1 (* r1 r0 83.0 83.0) r1 r1) 2426.0 2426.0 6618424257.0) v59 v7) (xor (>= (* r1 (* r1 r0 83.0 83.0) r1 r1) 2426.0 2426.0 6618424257.0) v59 v7)))
(assert (or v26 (and (and v12 v11 (>= 307769.0 r5) v40 (>= r6 (/ r0 (/ 83.0 r2)) (+ r1 r3 (* r1 r0 83.0 83.0) r2 r0) (* (- (* 26664.0 (* r1 r0 83.0 83.0) (/ r0 (/ 83.0 r2)) r1 (* r1 (* r1 r0 83.0 83.0) r1 r1)) 26664.0 83.0) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (<= (* (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)) r2 (* r1 (* r1 r0 83.0 83.0) r1 r1) (* r1 (* r1 r0 83.0 83.0) r1 r1) 6618424257.0) 2.0 (* (/ r0 (/ 83.0 r2)) 2.0 r6 (* r1 r0 83.0 83.0))) (<= (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1))) (/ r8 6618424257.0)) v30) (and (= (* r1 r0 83.0 83.0) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)) r1) (>= 83.0 r2 (* r1 (* r1 r0 83.0 83.0) r1 r1) r1 83.0) v1 v10 v18 (> r1 (* r1 r0 83.0 83.0) r2 r3 r3)) v52) (= (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)) (* (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)) r2 (* r1 (* r1 r0 83.0 83.0) r1 r1) (* r1 (* r1 r0 83.0 83.0) r1 r1) 6618424257.0) r2 (/ 83.0 (- r2)) (* (- (* 26664.0 (* r1 r0 83.0 83.0) (/ r0 (/ 83.0 r2)) r1 (* r1 (* r1 r0 83.0 83.0) r1 r1)) 26664.0 83.0) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1))))))
(assert (or (and (and v12 v11 (>= 307769.0 r5) v40 (>= r6 (/ r0 (/ 83.0 r2)) (+ r1 r3 (* r1 r0 83.0 83.0) r2 r0) (* (- (* 26664.0 (* r1 r0 83.0 83.0) (/ r0 (/ 83.0 r2)) r1 (* r1 (* r1 r0 83.0 83.0) r1 r1)) 26664.0 83.0) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (<= (* (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)) r2 (* r1 (* r1 r0 83.0 83.0) r1 r1) (* r1 (* r1 r0 83.0 83.0) r1 r1) 6618424257.0) 2.0 (* (/ r0 (/ 83.0 r2)) 2.0 r6 (* r1 r0 83.0 83.0))) (<= (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1))) (/ r8 6618424257.0)) v30) (and (= (* r1 r0 83.0 83.0) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)) r1) (>= 83.0 r2 (* r1 (* r1 r0 83.0 83.0) r1 r1) r1 83.0) v1 v10 v18 (> r1 (* r1 r0 83.0 83.0) r2 r3 r3)) v52) (<= (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (+ (- (* 26664.0 (* r1 r0 83.0 83.0) (/ r0 (/ 83.0 r2)) r1 (* r1 (* r1 r0 83.0 83.0) r1 r1)) 26664.0 83.0) (/ r8 6618424257.0) r2 26664.0) (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (/ r5 (/ (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (* 26664.0 (* r1 r0 83.0 83.0) (/ r0 (/ 83.0 r2)) r1 (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (* (- r2) (* r1 r0 83.0 83.0) r2 (/ 83.0 r2))) (<= 26664.0 (- r1))))
(assert (or v38 (< (- (* r1 r0 83.0 83.0)) (/ r8 6618424257.0)) v38))
(assert (or v30 (= (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)) (* (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)) r2 (* r1 (* r1 r0 83.0 83.0) r1 r1) (* r1 (* r1 r0 83.0 83.0) r1 r1) 6618424257.0) r2 (/ 83.0 (- r2)) (* (- (* 26664.0 (* r1 r0 83.0 83.0) (/ r0 (/ 83.0 r2)) r1 (* r1 (* r1 r0 83.0 83.0) r1 r1)) 26664.0 83.0) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) v5))
(assert (or (<= 26664.0 (- (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3))) v38 v44))
(assert (or v5 (<= 26664.0 (- r1)) (and (and v12 v11 (>= 307769.0 r5) v40 (>= r6 (/ r0 (/ 83.0 r2)) (+ r1 r3 (* r1 r0 83.0 83.0) r2 r0) (* (- (* 26664.0 (* r1 r0 83.0 83.0) (/ r0 (/ 83.0 r2)) r1 (* r1 (* r1 r0 83.0 83.0) r1 r1)) 26664.0 83.0) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (<= (* (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)) r2 (* r1 (* r1 r0 83.0 83.0) r1 r1) (* r1 (* r1 r0 83.0 83.0) r1 r1) 6618424257.0) 2.0 (* (/ r0 (/ 83.0 r2)) 2.0 r6 (* r1 r0 83.0 83.0))) (<= (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1))) (/ r8 6618424257.0)) v30) (and (= (* r1 r0 83.0 83.0) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)) r1) (>= 83.0 r2 (* r1 (* r1 r0 83.0 83.0) r1 r1) r1 83.0) v1 v10 v18 (> r1 (* r1 r0 83.0 83.0) r2 r3 r3)) v52)))
(assert (or (< (- (* r1 r0 83.0 83.0)) (/ r8 6618424257.0)) v30 (xor (>= (* r1 (* r1 r0 83.0 83.0) r1 r1) 2426.0 2426.0 6618424257.0) v59 v7)))
(assert (or (distinct (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1))))) v5 v44))
(assert (or v44 (>= (/ r2 (* (/ r0 (/ 83.0 r2)) 2.0 r6 (* r1 r0 83.0 83.0))) r4 (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (/ (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (* 26664.0 (* r1 r0 83.0 83.0) (/ r0 (/ 83.0 r2)) r1 (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (<= 26664.0 (- r1))))
(assert (or (and (and v12 v11 (>= 307769.0 r5) v40 (>= r6 (/ r0 (/ 83.0 r2)) (+ r1 r3 (* r1 r0 83.0 83.0) r2 r0) (* (- (* 26664.0 (* r1 r0 83.0 83.0) (/ r0 (/ 83.0 r2)) r1 (* r1 (* r1 r0 83.0 83.0) r1 r1)) 26664.0 83.0) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (<= (* (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)) r2 (* r1 (* r1 r0 83.0 83.0) r1 r1) (* r1 (* r1 r0 83.0 83.0) r1 r1) 6618424257.0) 2.0 (* (/ r0 (/ 83.0 r2)) 2.0 r6 (* r1 r0 83.0 83.0))) (<= (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1))) (/ r8 6618424257.0)) v30) (and (= (* r1 r0 83.0 83.0) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)) r1) (>= 83.0 r2 (* r1 (* r1 r0 83.0 83.0) r1 r1) r1 83.0) v1 v10 v18 (> r1 (* r1 r0 83.0 83.0) r2 r3 r3)) v52) (>= (/ r2 (* (/ r0 (/ 83.0 r2)) 2.0 r6 (* r1 r0 83.0 83.0))) r4 (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (/ (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (* 26664.0 (* r1 r0 83.0 83.0) (/ r0 (/ 83.0 r2)) r1 (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (< (- (* r1 r0 83.0 83.0)) (/ r8 6618424257.0))))
(assert (or (xor (>= (* r1 (* r1 r0 83.0 83.0) r1 r1) 2426.0 2426.0 6618424257.0) v59 v7) (xor (>= (* r1 (* r1 r0 83.0 83.0) r1 r1) 2426.0 2426.0 6618424257.0) v59 v7) v30))
(assert (or (>= (/ r2 (* (/ r0 (/ 83.0 r2)) 2.0 r6 (* r1 r0 83.0 83.0))) r4 (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (/ (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (* 26664.0 (* r1 r0 83.0 83.0) (/ r0 (/ 83.0 r2)) r1 (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (>= (/ r2 (* (/ r0 (/ 83.0 r2)) 2.0 r6 (* r1 r0 83.0 83.0))) r4 (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (/ (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (* 26664.0 (* r1 r0 83.0 83.0) (/ r0 (/ 83.0 r2)) r1 (* r1 (* r1 r0 83.0 83.0) r1 r1)))) v39))
(assert (or (<= 26664.0 (- (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3))) (<= 26664.0 (- (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3))) v39))
(assert (or (< (- (* r1 r0 83.0 83.0)) (/ r8 6618424257.0)) v60 (>= (/ r2 (* (/ r0 (/ 83.0 r2)) 2.0 r6 (* r1 r0 83.0 83.0))) r4 (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (/ (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (* 26664.0 (* r1 r0 83.0 83.0) (/ r0 (/ 83.0 r2)) r1 (* r1 (* r1 r0 83.0 83.0) r1 r1))))))
(assert (or v26 (and (and v12 v11 (>= 307769.0 r5) v40 (>= r6 (/ r0 (/ 83.0 r2)) (+ r1 r3 (* r1 r0 83.0 83.0) r2 r0) (* (- (* 26664.0 (* r1 r0 83.0 83.0) (/ r0 (/ 83.0 r2)) r1 (* r1 (* r1 r0 83.0 83.0) r1 r1)) 26664.0 83.0) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (<= (* (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)) r2 (* r1 (* r1 r0 83.0 83.0) r1 r1) (* r1 (* r1 r0 83.0 83.0) r1 r1) 6618424257.0) 2.0 (* (/ r0 (/ 83.0 r2)) 2.0 r6 (* r1 r0 83.0 83.0))) (<= (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1))) (/ r8 6618424257.0)) v30) (and (= (* r1 r0 83.0 83.0) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)) r1) (>= 83.0 r2 (* r1 (* r1 r0 83.0 83.0) r1 r1) r1 83.0) v1 v10 v18 (> r1 (* r1 r0 83.0 83.0) r2 r3 r3)) v52) (<= 26664.0 (- r1))))
(assert (or (xor (>= (* r1 (* r1 r0 83.0 83.0) r1 r1) 2426.0 2426.0 6618424257.0) v59 v7) (= (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)) (* (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)) r2 (* r1 (* r1 r0 83.0 83.0) r1 r1) (* r1 (* r1 r0 83.0 83.0) r1 r1) 6618424257.0) r2 (/ 83.0 (- r2)) (* (- (* 26664.0 (* r1 r0 83.0 83.0) (/ r0 (/ 83.0 r2)) r1 (* r1 (* r1 r0 83.0 83.0) r1 r1)) 26664.0 83.0) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (<= 26664.0 (- (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3)))))
(assert (or v39 (>= (/ r2 (* (/ r0 (/ 83.0 r2)) 2.0 r6 (* r1 r0 83.0 83.0))) r4 (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (/ (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (* 26664.0 (* r1 r0 83.0 83.0) (/ r0 (/ 83.0 r2)) r1 (* r1 (* r1 r0 83.0 83.0) r1 r1)))) v39))
(assert (or (= (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)) (* (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)) r2 (* r1 (* r1 r0 83.0 83.0) r1 r1) (* r1 (* r1 r0 83.0 83.0) r1 r1) 6618424257.0) r2 (/ 83.0 (- r2)) (* (- (* 26664.0 (* r1 r0 83.0 83.0) (/ r0 (/ 83.0 r2)) r1 (* r1 (* r1 r0 83.0 83.0) r1 r1)) 26664.0 83.0) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (<= 26664.0 (- r1)) (< (- (* r1 r0 83.0 83.0)) (/ r8 6618424257.0))))
(assert (or (< (- (* r1 r0 83.0 83.0)) (/ r8 6618424257.0)) (< (- (* r1 r0 83.0 83.0)) (/ r8 6618424257.0)) v38))
(assert (or (distinct (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1))))) (= (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)) (* (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)) r2 (* r1 (* r1 r0 83.0 83.0) r1 r1) (* r1 (* r1 r0 83.0 83.0) r1 r1) 6618424257.0) r2 (/ 83.0 (- r2)) (* (- (* 26664.0 (* r1 r0 83.0 83.0) (/ r0 (/ 83.0 r2)) r1 (* r1 (* r1 r0 83.0 83.0) r1 r1)) 26664.0 83.0) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (xor (>= (* r1 (* r1 r0 83.0 83.0) r1 r1) 2426.0 2426.0 6618424257.0) v59 v7)))
(assert (or (and (and v12 v11 (>= 307769.0 r5) v40 (>= r6 (/ r0 (/ 83.0 r2)) (+ r1 r3 (* r1 r0 83.0 83.0) r2 r0) (* (- (* 26664.0 (* r1 r0 83.0 83.0) (/ r0 (/ 83.0 r2)) r1 (* r1 (* r1 r0 83.0 83.0) r1 r1)) 26664.0 83.0) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (<= (* (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)) r2 (* r1 (* r1 r0 83.0 83.0) r1 r1) (* r1 (* r1 r0 83.0 83.0) r1 r1) 6618424257.0) 2.0 (* (/ r0 (/ 83.0 r2)) 2.0 r6 (* r1 r0 83.0 83.0))) (<= (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1))) (/ r8 6618424257.0)) v30) (and (= (* r1 r0 83.0 83.0) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)) r1) (>= 83.0 r2 (* r1 (* r1 r0 83.0 83.0) r1 r1) r1 83.0) v1 v10 v18 (> r1 (* r1 r0 83.0 83.0) r2 r3 r3)) v52) v38 v5))
(assert (or (< (- (* r1 r0 83.0 83.0)) (/ r8 6618424257.0)) (<= 26664.0 (- r1)) v38))
(assert (or (<= 26664.0 (- (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3))) v38 v30))
(assert (or v5 v26 v60))
(assert (or (xor (>= (* r1 (* r1 r0 83.0 83.0) r1 r1) 2426.0 2426.0 6618424257.0) v59 v7) v60 (xor (>= (* r1 (* r1 r0 83.0 83.0) r1 r1) 2426.0 2426.0 6618424257.0) v59 v7)))
(assert (or (>= (/ r2 (* (/ r0 (/ 83.0 r2)) 2.0 r6 (* r1 r0 83.0 83.0))) r4 (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (/ (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (* 26664.0 (* r1 r0 83.0 83.0) (/ r0 (/ 83.0 r2)) r1 (* r1 (* r1 r0 83.0 83.0) r1 r1)))) v39 (= (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)) (* (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)) r2 (* r1 (* r1 r0 83.0 83.0) r1 r1) (* r1 (* r1 r0 83.0 83.0) r1 r1) 6618424257.0) r2 (/ 83.0 (- r2)) (* (- (* 26664.0 (* r1 r0 83.0 83.0) (/ r0 (/ 83.0 r2)) r1 (* r1 (* r1 r0 83.0 83.0) r1 r1)) 26664.0 83.0) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1))))))
(assert (or v39 v44 (<= (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (+ (- (* 26664.0 (* r1 r0 83.0 83.0) (/ r0 (/ 83.0 r2)) r1 (* r1 (* r1 r0 83.0 83.0) r1 r1)) 26664.0 83.0) (/ r8 6618424257.0) r2 26664.0) (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (/ r5 (/ (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (* 26664.0 (* r1 r0 83.0 83.0) (/ r0 (/ 83.0 r2)) r1 (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (* (- r2) (* r1 r0 83.0 83.0) r2 (/ 83.0 r2)))))
(assert (or v26 (and (and v12 v11 (>= 307769.0 r5) v40 (>= r6 (/ r0 (/ 83.0 r2)) (+ r1 r3 (* r1 r0 83.0 83.0) r2 r0) (* (- (* 26664.0 (* r1 r0 83.0 83.0) (/ r0 (/ 83.0 r2)) r1 (* r1 (* r1 r0 83.0 83.0) r1 r1)) 26664.0 83.0) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (<= (* (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)) r2 (* r1 (* r1 r0 83.0 83.0) r1 r1) (* r1 (* r1 r0 83.0 83.0) r1 r1) 6618424257.0) 2.0 (* (/ r0 (/ 83.0 r2)) 2.0 r6 (* r1 r0 83.0 83.0))) (<= (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1))) (/ r8 6618424257.0)) v30) (and (= (* r1 r0 83.0 83.0) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)) r1) (>= 83.0 r2 (* r1 (* r1 r0 83.0 83.0) r1 r1) r1 83.0) v1 v10 v18 (> r1 (* r1 r0 83.0 83.0) r2 r3 r3)) v52) (< (- (* r1 r0 83.0 83.0)) (/ r8 6618424257.0))))
(assert (or v26 (< (- (* r1 r0 83.0 83.0)) (/ r8 6618424257.0)) (and (and v12 v11 (>= 307769.0 r5) v40 (>= r6 (/ r0 (/ 83.0 r2)) (+ r1 r3 (* r1 r0 83.0 83.0) r2 r0) (* (- (* 26664.0 (* r1 r0 83.0 83.0) (/ r0 (/ 83.0 r2)) r1 (* r1 (* r1 r0 83.0 83.0) r1 r1)) 26664.0 83.0) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (<= (* (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)) r2 (* r1 (* r1 r0 83.0 83.0) r1 r1) (* r1 (* r1 r0 83.0 83.0) r1 r1) 6618424257.0) 2.0 (* (/ r0 (/ 83.0 r2)) 2.0 r6 (* r1 r0 83.0 83.0))) (<= (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1))) (/ r8 6618424257.0)) v30) (and (= (* r1 r0 83.0 83.0) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)) r1) (>= 83.0 r2 (* r1 (* r1 r0 83.0 83.0) r1 r1) r1 83.0) v1 v10 v18 (> r1 (* r1 r0 83.0 83.0) r2 r3 r3)) v52)))
(assert (or v38 v38 (<= 26664.0 (- r1))))
(assert (or (xor (>= (* r1 (* r1 r0 83.0 83.0) r1 r1) 2426.0 2426.0 6618424257.0) v59 v7) v5 (xor (>= (* r1 (* r1 r0 83.0 83.0) r1 r1) 2426.0 2426.0 6618424257.0) v59 v7)))
(assert (or (< (- (* r1 r0 83.0 83.0)) (/ r8 6618424257.0)) v5 (= (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)) (* (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)) r2 (* r1 (* r1 r0 83.0 83.0) r1 r1) (* r1 (* r1 r0 83.0 83.0) r1 r1) 6618424257.0) r2 (/ 83.0 (- r2)) (* (- (* 26664.0 (* r1 r0 83.0 83.0) (/ r0 (/ 83.0 r2)) r1 (* r1 (* r1 r0 83.0 83.0) r1 r1)) 26664.0 83.0) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1))))))
(assert (or v39 (distinct (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1))))) v30))
(assert (or v38 (<= 26664.0 (- r1)) (and (and v12 v11 (>= 307769.0 r5) v40 (>= r6 (/ r0 (/ 83.0 r2)) (+ r1 r3 (* r1 r0 83.0 83.0) r2 r0) (* (- (* 26664.0 (* r1 r0 83.0 83.0) (/ r0 (/ 83.0 r2)) r1 (* r1 (* r1 r0 83.0 83.0) r1 r1)) 26664.0 83.0) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (<= (* (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)) r2 (* r1 (* r1 r0 83.0 83.0) r1 r1) (* r1 (* r1 r0 83.0 83.0) r1 r1) 6618424257.0) 2.0 (* (/ r0 (/ 83.0 r2)) 2.0 r6 (* r1 r0 83.0 83.0))) (<= (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1))) (/ r8 6618424257.0)) v30) (and (= (* r1 r0 83.0 83.0) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)) r1) (>= 83.0 r2 (* r1 (* r1 r0 83.0 83.0) r1 r1) r1 83.0) v1 v10 v18 (> r1 (* r1 r0 83.0 83.0) r2 r3 r3)) v52)))
(assert (or v44 (<= 26664.0 (- r1)) (<= 26664.0 (- (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3)))))
(assert (or v60 (<= 26664.0 (- (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3))) (<= 26664.0 (- r1))))
(assert (or (<= 26664.0 (- (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3))) (<= 26664.0 (- (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3))) v44))
(assert (or (<= 26664.0 (- r1)) v38 v30))
(assert (or v5 (<= (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (+ (- (* 26664.0 (* r1 r0 83.0 83.0) (/ r0 (/ 83.0 r2)) r1 (* r1 (* r1 r0 83.0 83.0) r1 r1)) 26664.0 83.0) (/ r8 6618424257.0) r2 26664.0) (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (/ r5 (/ (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (* 26664.0 (* r1 r0 83.0 83.0) (/ r0 (/ 83.0 r2)) r1 (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (* (- r2) (* r1 r0 83.0 83.0) r2 (/ 83.0 r2))) v39))
(assert (or v44 v44 v44))
(assert (or (<= 26664.0 (- r1)) v38 (>= (/ r2 (* (/ r0 (/ 83.0 r2)) 2.0 r6 (* r1 r0 83.0 83.0))) r4 (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (/ (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (* 26664.0 (* r1 r0 83.0 83.0) (/ r0 (/ 83.0 r2)) r1 (* r1 (* r1 r0 83.0 83.0) r1 r1))))))
(assert (or v44 v38 (< (- (* r1 r0 83.0 83.0)) (/ r8 6618424257.0))))
(assert (or v26 (< (- (* r1 r0 83.0 83.0)) (/ r8 6618424257.0)) (distinct (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))))))
(assert (or v26 v39 v44))
(assert (or v38 (and (and v12 v11 (>= 307769.0 r5) v40 (>= r6 (/ r0 (/ 83.0 r2)) (+ r1 r3 (* r1 r0 83.0 83.0) r2 r0) (* (- (* 26664.0 (* r1 r0 83.0 83.0) (/ r0 (/ 83.0 r2)) r1 (* r1 (* r1 r0 83.0 83.0) r1 r1)) 26664.0 83.0) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (<= (* (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)) r2 (* r1 (* r1 r0 83.0 83.0) r1 r1) (* r1 (* r1 r0 83.0 83.0) r1 r1) 6618424257.0) 2.0 (* (/ r0 (/ 83.0 r2)) 2.0 r6 (* r1 r0 83.0 83.0))) (<= (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1))) (/ r8 6618424257.0)) v30) (and (= (* r1 r0 83.0 83.0) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)) r1) (>= 83.0 r2 (* r1 (* r1 r0 83.0 83.0) r1 r1) r1 83.0) v1 v10 v18 (> r1 (* r1 r0 83.0 83.0) r2 r3 r3)) v52) (and (and v12 v11 (>= 307769.0 r5) v40 (>= r6 (/ r0 (/ 83.0 r2)) (+ r1 r3 (* r1 r0 83.0 83.0) r2 r0) (* (- (* 26664.0 (* r1 r0 83.0 83.0) (/ r0 (/ 83.0 r2)) r1 (* r1 (* r1 r0 83.0 83.0) r1 r1)) 26664.0 83.0) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (<= (* (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)) r2 (* r1 (* r1 r0 83.0 83.0) r1 r1) (* r1 (* r1 r0 83.0 83.0) r1 r1) 6618424257.0) 2.0 (* (/ r0 (/ 83.0 r2)) 2.0 r6 (* r1 r0 83.0 83.0))) (<= (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1))) (/ r8 6618424257.0)) v30) (and (= (* r1 r0 83.0 83.0) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)) r1) (>= 83.0 r2 (* r1 (* r1 r0 83.0 83.0) r1 r1) r1 83.0) v1 v10 v18 (> r1 (* r1 r0 83.0 83.0) r2 r3 r3)) v52)))
(assert (or (< (- (* r1 r0 83.0 83.0)) (/ r8 6618424257.0)) (<= 26664.0 (- r1)) v39))
(assert (or v60 (= (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)) (* (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)) r2 (* r1 (* r1 r0 83.0 83.0) r1 r1) (* r1 (* r1 r0 83.0 83.0) r1 r1) 6618424257.0) r2 (/ 83.0 (- r2)) (* (- (* 26664.0 (* r1 r0 83.0 83.0) (/ r0 (/ 83.0 r2)) r1 (* r1 (* r1 r0 83.0 83.0) r1 r1)) 26664.0 83.0) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (<= 26664.0 (- r1))))
(assert (or v30 v5 (xor (>= (* r1 (* r1 r0 83.0 83.0) r1 r1) 2426.0 2426.0 6618424257.0) v59 v7)))
(assert (or v5 v44 (<= (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (+ (- (* 26664.0 (* r1 r0 83.0 83.0) (/ r0 (/ 83.0 r2)) r1 (* r1 (* r1 r0 83.0 83.0) r1 r1)) 26664.0 83.0) (/ r8 6618424257.0) r2 26664.0) (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (/ r5 (/ (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (* 26664.0 (* r1 r0 83.0 83.0) (/ r0 (/ 83.0 r2)) r1 (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (* (- r2) (* r1 r0 83.0 83.0) r2 (/ 83.0 r2)))))
(assert (or v38 (and (and v12 v11 (>= 307769.0 r5) v40 (>= r6 (/ r0 (/ 83.0 r2)) (+ r1 r3 (* r1 r0 83.0 83.0) r2 r0) (* (- (* 26664.0 (* r1 r0 83.0 83.0) (/ r0 (/ 83.0 r2)) r1 (* r1 (* r1 r0 83.0 83.0) r1 r1)) 26664.0 83.0) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (<= (* (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)) r2 (* r1 (* r1 r0 83.0 83.0) r1 r1) (* r1 (* r1 r0 83.0 83.0) r1 r1) 6618424257.0) 2.0 (* (/ r0 (/ 83.0 r2)) 2.0 r6 (* r1 r0 83.0 83.0))) (<= (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1))) (/ r8 6618424257.0)) v30) (and (= (* r1 r0 83.0 83.0) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)) r1) (>= 83.0 r2 (* r1 (* r1 r0 83.0 83.0) r1 r1) r1 83.0) v1 v10 v18 (> r1 (* r1 r0 83.0 83.0) r2 r3 r3)) v52) v5))
(assert (or (>= (/ r2 (* (/ r0 (/ 83.0 r2)) 2.0 r6 (* r1 r0 83.0 83.0))) r4 (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (/ (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (* 26664.0 (* r1 r0 83.0 83.0) (/ r0 (/ 83.0 r2)) r1 (* r1 (* r1 r0 83.0 83.0) r1 r1)))) v39 v5))
(assert (or (xor (>= (* r1 (* r1 r0 83.0 83.0) r1 r1) 2426.0 2426.0 6618424257.0) v59 v7) (< (- (* r1 r0 83.0 83.0)) (/ r8 6618424257.0)) v30))
(assert (or (xor (>= (* r1 (* r1 r0 83.0 83.0) r1 r1) 2426.0 2426.0 6618424257.0) v59 v7) v39 v26))
(assert (or v44 (and (and v12 v11 (>= 307769.0 r5) v40 (>= r6 (/ r0 (/ 83.0 r2)) (+ r1 r3 (* r1 r0 83.0 83.0) r2 r0) (* (- (* 26664.0 (* r1 r0 83.0 83.0) (/ r0 (/ 83.0 r2)) r1 (* r1 (* r1 r0 83.0 83.0) r1 r1)) 26664.0 83.0) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (<= (* (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)) r2 (* r1 (* r1 r0 83.0 83.0) r1 r1) (* r1 (* r1 r0 83.0 83.0) r1 r1) 6618424257.0) 2.0 (* (/ r0 (/ 83.0 r2)) 2.0 r6 (* r1 r0 83.0 83.0))) (<= (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1))) (/ r8 6618424257.0)) v30) (and (= (* r1 r0 83.0 83.0) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)) r1) (>= 83.0 r2 (* r1 (* r1 r0 83.0 83.0) r1 r1) r1 83.0) v1 v10 v18 (> r1 (* r1 r0 83.0 83.0) r2 r3 r3)) v52) (>= (/ r2 (* (/ r0 (/ 83.0 r2)) 2.0 r6 (* r1 r0 83.0 83.0))) r4 (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (/ (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (* 26664.0 (* r1 r0 83.0 83.0) (/ r0 (/ 83.0 r2)) r1 (* r1 (* r1 r0 83.0 83.0) r1 r1))))))
(assert (or (= (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)) (* (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)) r2 (* r1 (* r1 r0 83.0 83.0) r1 r1) (* r1 (* r1 r0 83.0 83.0) r1 r1) 6618424257.0) r2 (/ 83.0 (- r2)) (* (- (* 26664.0 (* r1 r0 83.0 83.0) (/ r0 (/ 83.0 r2)) r1 (* r1 (* r1 r0 83.0 83.0) r1 r1)) 26664.0 83.0) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (and (and v12 v11 (>= 307769.0 r5) v40 (>= r6 (/ r0 (/ 83.0 r2)) (+ r1 r3 (* r1 r0 83.0 83.0) r2 r0) (* (- (* 26664.0 (* r1 r0 83.0 83.0) (/ r0 (/ 83.0 r2)) r1 (* r1 (* r1 r0 83.0 83.0) r1 r1)) 26664.0 83.0) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (<= (* (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)) r2 (* r1 (* r1 r0 83.0 83.0) r1 r1) (* r1 (* r1 r0 83.0 83.0) r1 r1) 6618424257.0) 2.0 (* (/ r0 (/ 83.0 r2)) 2.0 r6 (* r1 r0 83.0 83.0))) (<= (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1))) (/ r8 6618424257.0)) v30) (and (= (* r1 r0 83.0 83.0) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)) r1) (>= 83.0 r2 (* r1 (* r1 r0 83.0 83.0) r1 r1) r1 83.0) v1 v10 v18 (> r1 (* r1 r0 83.0 83.0) r2 r3 r3)) v52) v39))
(assert (or v30 v26 (= (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)) (* (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)) r2 (* r1 (* r1 r0 83.0 83.0) r1 r1) (* r1 (* r1 r0 83.0 83.0) r1 r1) 6618424257.0) r2 (/ 83.0 (- r2)) (* (- (* 26664.0 (* r1 r0 83.0 83.0) (/ r0 (/ 83.0 r2)) r1 (* r1 (* r1 r0 83.0 83.0) r1 r1)) 26664.0 83.0) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1))))))
(assert (or v38 (<= 26664.0 (- (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3))) (<= (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (+ (- (* 26664.0 (* r1 r0 83.0 83.0) (/ r0 (/ 83.0 r2)) r1 (* r1 (* r1 r0 83.0 83.0) r1 r1)) 26664.0 83.0) (/ r8 6618424257.0) r2 26664.0) (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (/ r5 (/ (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (* 26664.0 (* r1 r0 83.0 83.0) (/ r0 (/ 83.0 r2)) r1 (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (* (- r2) (* r1 r0 83.0 83.0) r2 (/ 83.0 r2)))))
(assert (or (= (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)) (* (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)) r2 (* r1 (* r1 r0 83.0 83.0) r1 r1) (* r1 (* r1 r0 83.0 83.0) r1 r1) 6618424257.0) r2 (/ 83.0 (- r2)) (* (- (* 26664.0 (* r1 r0 83.0 83.0) (/ r0 (/ 83.0 r2)) r1 (* r1 (* r1 r0 83.0 83.0) r1 r1)) 26664.0 83.0) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (= (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)) (* (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)) r2 (* r1 (* r1 r0 83.0 83.0) r1 r1) (* r1 (* r1 r0 83.0 83.0) r1 r1) 6618424257.0) r2 (/ 83.0 (- r2)) (* (- (* 26664.0 (* r1 r0 83.0 83.0) (/ r0 (/ 83.0 r2)) r1 (* r1 (* r1 r0 83.0 83.0) r1 r1)) 26664.0 83.0) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) v39))
(assert (or (and (and v12 v11 (>= 307769.0 r5) v40 (>= r6 (/ r0 (/ 83.0 r2)) (+ r1 r3 (* r1 r0 83.0 83.0) r2 r0) (* (- (* 26664.0 (* r1 r0 83.0 83.0) (/ r0 (/ 83.0 r2)) r1 (* r1 (* r1 r0 83.0 83.0) r1 r1)) 26664.0 83.0) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (<= (* (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)) r2 (* r1 (* r1 r0 83.0 83.0) r1 r1) (* r1 (* r1 r0 83.0 83.0) r1 r1) 6618424257.0) 2.0 (* (/ r0 (/ 83.0 r2)) 2.0 r6 (* r1 r0 83.0 83.0))) (<= (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1))) (/ r8 6618424257.0)) v30) (and (= (* r1 r0 83.0 83.0) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)) r1) (>= 83.0 r2 (* r1 (* r1 r0 83.0 83.0) r1 r1) r1 83.0) v1 v10 v18 (> r1 (* r1 r0 83.0 83.0) r2 r3 r3)) v52) (<= 26664.0 (- r1)) (distinct (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))))))
(assert (or v39 (xor (>= (* r1 (* r1 r0 83.0 83.0) r1 r1) 2426.0 2426.0 6618424257.0) v59 v7) v60))
(assert (or (<= (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (+ (- (* 26664.0 (* r1 r0 83.0 83.0) (/ r0 (/ 83.0 r2)) r1 (* r1 (* r1 r0 83.0 83.0) r1 r1)) 26664.0 83.0) (/ r8 6618424257.0) r2 26664.0) (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (/ r5 (/ (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (* 26664.0 (* r1 r0 83.0 83.0) (/ r0 (/ 83.0 r2)) r1 (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (* (- r2) (* r1 r0 83.0 83.0) r2 (/ 83.0 r2))) (<= 26664.0 (- r1)) v39))
(assert (or (xor (>= (* r1 (* r1 r0 83.0 83.0) r1 r1) 2426.0 2426.0 6618424257.0) v59 v7) v60 v38))
(assert (or v39 v26 v60))
(assert (or v26 (distinct (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1))))) v26))
(assert (or v44 v26 v60))
(assert (or (distinct (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1))))) v5 (<= (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (+ (- (* 26664.0 (* r1 r0 83.0 83.0) (/ r0 (/ 83.0 r2)) r1 (* r1 (* r1 r0 83.0 83.0) r1 r1)) 26664.0 83.0) (/ r8 6618424257.0) r2 26664.0) (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (/ r5 (/ (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (* 26664.0 (* r1 r0 83.0 83.0) (/ r0 (/ 83.0 r2)) r1 (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (* (- r2) (* r1 r0 83.0 83.0) r2 (/ 83.0 r2)))))
(assert (or (= (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)) (* (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)) r2 (* r1 (* r1 r0 83.0 83.0) r1 r1) (* r1 (* r1 r0 83.0 83.0) r1 r1) 6618424257.0) r2 (/ 83.0 (- r2)) (* (- (* 26664.0 (* r1 r0 83.0 83.0) (/ r0 (/ 83.0 r2)) r1 (* r1 (* r1 r0 83.0 83.0) r1 r1)) 26664.0 83.0) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) v30 (= (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)) (* (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)) r2 (* r1 (* r1 r0 83.0 83.0) r1 r1) (* r1 (* r1 r0 83.0 83.0) r1 r1) 6618424257.0) r2 (/ 83.0 (- r2)) (* (- (* 26664.0 (* r1 r0 83.0 83.0) (/ r0 (/ 83.0 r2)) r1 (* r1 (* r1 r0 83.0 83.0) r1 r1)) 26664.0 83.0) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1))))))
(assert (or (= (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)) (* (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)) r2 (* r1 (* r1 r0 83.0 83.0) r1 r1) (* r1 (* r1 r0 83.0 83.0) r1 r1) 6618424257.0) r2 (/ 83.0 (- r2)) (* (- (* 26664.0 (* r1 r0 83.0 83.0) (/ r0 (/ 83.0 r2)) r1 (* r1 (* r1 r0 83.0 83.0) r1 r1)) 26664.0 83.0) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) v38 v39))
(assert (or v5 v44 v30))
(assert (or v26 v5 v5))
(assert (or (< (- (* r1 r0 83.0 83.0)) (/ r8 6618424257.0)) (<= (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (+ (- (* 26664.0 (* r1 r0 83.0 83.0) (/ r0 (/ 83.0 r2)) r1 (* r1 (* r1 r0 83.0 83.0) r1 r1)) 26664.0 83.0) (/ r8 6618424257.0) r2 26664.0) (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (/ r5 (/ (- (/ (/ (* r1 (* r1 r0 83.0 83.0) r1 r1) r3) (/ (* r1 r0 83.0 83.0) (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (* 26664.0 (* r1 r0 83.0 83.0) (/ r0 (/ 83.0 r2)) r1 (* r1 (* r1 r0 83.0 83.0) r1 r1)))) (* (- r2) (* r1 r0 83.0 83.0) r2 (/ 83.0 r2))) v5))
(assert (or v38 v5 v60))
(check-sat)
(exit)
